fix #2595

NikolajBjorner · NikolajBjorner · commit 301209cda648 · 2019-09-28T17:44:25.000-07:00
Signed-off-by: Nikolaj Bjorner &lt;nbjorner@microsoft.com&gt;
diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp
@@ -2384,8 +2384,6 @@ namespace polynomial {
 
         void checkpoint() {
             if (!m_limit.inc()) {
-                m_som_buffer.reset();
-                m_som_buffer2.reset();
                 throw polynomial_exception(Z3_CANCELED_MSG);
             }
         }

Original file line number	Diff line number	Diff line change
`@@ -2384,8 +2384,6 @@ namespace polynomial {`
`2384`	`2384`
`2385`	`2385`	`void checkpoint() {`
`2386`	`2386`	`if (!m_limit.inc()) {`
`2387`		`- m_som_buffer.reset();`
`2388`		`- m_som_buffer2.reset();`
`2389`	`2387`	`throw polynomial_exception(Z3_CANCELED_MSG);`
`2390`	`2388`	`}`
`2391`	`2389`	`}`