From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 3 Nov 2020 18:17:32 +0000 (-0600)
Subject: Reset built model flag at presolve in nonlinear (#5386)
X-Git-Tag: cvc5-1.0.0~2636
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e2aff722e0b1072e90bd0c77e7030957364283cc;p=cvc5.git

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 fdab6d7b7..f5e83c8f0 100644
--- 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 98fde9847..3bce17525 100644
--- 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
index 000000000..35abe223a
--- /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)