Reset built model flag at presolve in nonlinear (#5386)

Fixes a bug in incremental with non-linear where the built model flag would still be true on the first call to check in a 2nd call to check-sat in incremental mode. This occurs when we are under the same SAT context when the model was built (likely level 0) on the subsequent check-sat call.

Fixes #5372

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index fdab6d7b73d1aaecd9bc624d7186b01325b3406c..f5e83c8f0abd7dc7e4a33cbf00dec57a83202b06 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -582,6 +582,7 @@ void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel)
 void NonlinearExtension::presolve()
 {
   Trace("nl-ext") << "NonlinearExtension::presolve" << std::endl;
+  d_builtModel = false;
 }
 
 void NonlinearExtension::runStrategy(Theory::Effort effort,

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 98fde98470a82108e033a29df18b33289576e373..3bce17525f329154a6798530557cd1309b06951f 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1445,6 +1445,7 @@ set(regress_1_tests
   regress1/nl/issue3656.smt2
   regress1/nl/issue3803-nl-check-model.smt2
   regress1/nl/issue3955-ee-double-notify.smt2
+  regress1/nl/issue5372-2-no-m-presolve.smt2
   regress1/nl/metitarski-1025.smt2
   regress1/nl/metitarski-3-4.smt2
   regress1/nl/metitarski_3_4_2e.smt2

diff --git a/test/regress/regress1/nl/issue5372-2-no-m-presolve.smt2 b/test/regress/regress1/nl/issue5372-2-no-m-presolve.smt2
new file mode 100644 (file)
index 0000000..35abe22
--- /dev/null
+++ b/test/regress/regress1/nl/issue5372-2-no-m-presolve.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun i4 () Int)
+(declare-fun i6 () Int)
+(declare-fun i7 () Int)
+(assert (= true true true (< i7 (* i4 i4)) true true true true))
+(check-sat)
+(assert (< i6 (* 51 51 i4 i6) 0 74))
+(check-sat)