Fix issue related to sanity checking integer models (#7363)

We now insist that we sanity check integer models in linear logics. Previously, we could trigger an assertion failure in Minisat if a user asked for a model in a state where the linear solver had assigned a real value to an integer variable, as we would be sending a lemma during collectModelValues in a state where we had already terminated with "sat".

This also changes an assertion to warning, to allow the regression to pass.

Fixes #6774 (This PR fixes a followup issue after the original bad model reported there was fixed by sanity checks).

As the assertion failure is downgraded to a warning, fixes #6988, fixes #7252.

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 76a0c363dc668f8b95a8e747b5e99af64fa02066..cf2373b9fa6535f621c594e5a624aad9eb0a3f79 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -193,9 +193,9 @@ void TheoryArith::postCheck(Effort level)
   if (Theory::fullEffort(level))
   {
     d_arithModelCache.clear();
+    std::set<Node> termSet;
     if (d_nonlinearExtension != nullptr)
     {
-      std::set<Node> termSet;
       updateModelCache(termSet);
       d_nonlinearExtension->checkFullEffort(d_arithModelCache, termSet);
     }
@@ -204,6 +204,15 @@ void TheoryArith::postCheck(Effort level)
       // set incomplete
       d_im.setIncomplete(IncompleteId::ARITH_NL_DISABLED);
     }
+    // If we won't be doing a last call effort check (which implies that
+    // models will be computed), we must sanity check the integer model
+    // from the linear solver now. We also must update the model cache
+    // if we did not do so above.
+    if (d_nonlinearExtension == nullptr)
+    {
+      updateModelCache(termSet);
+    }
+    sanityCheckIntegerModel();
   }
 }
 
@@ -274,12 +283,6 @@ bool TheoryArith::collectModelValues(TheoryModel* m,
 
   updateModelCache(termSet);
 
-  if (sanityCheckIntegerModel())
-  {
-    // We added a lemma
-    return false;
-  }
-
   // We are now ready to assert the model.
   for (const std::pair<const Node, Node>& p : d_arithModelCache)
   {
@@ -383,9 +386,9 @@ bool TheoryArith::sanityCheckIntegerModel()
       Trace("arith-check") << p.first << " -> " << p.second << std::endl;
       if (p.first.getType().isInteger() && !p.second.getType().isInteger())
       {
-        Assert(false) << "TheoryArithPrivate generated a bad model value for "
-                        "integer variable "
-                      << p.first << " : " << p.second;
+        Warning() << "TheoryArithPrivate generated a bad model value for "
+                     "integer variable "
+                  << p.first << " : " << p.second;
         // must branch and bound
         TrustNode lem =
             d_bab.branchIntegerVariable(p.first, p.second.getConst<Rational>());

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b1d776b21a256524be6c22724af187f2f64392ef..84f0ef408004ab421643bb7e056c2e6fe2a3857d 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1505,6 +1505,8 @@ set(regress_1_tests
   regress1/arith/issue3952-rew-eq.smt2
   regress1/arith/issue4985-model-success.smt2
   regress1/arith/issue4985b-model-success.smt2
+  regress1/arith/issue6774-sanity-int-model.smt2
+  regress1/arith/issue7252-arith-sanity.smt2
   regress1/arith/issue789.smt2
   regress1/arith/miplib3.cvc.smt2
   regress1/arith/mod.02.smt2
@@ -1576,6 +1578,7 @@ set(regress_1_tests
   regress1/constarr3.cvc.smt2
   regress1/constarr3.smt2
   regress1/cores/issue5604.smt2
+  regress1/cores/issue6988-arith-sanity.smt2
   regress1/datatypes/acyclicity-sr-ground096.smt2
   regress1/datatypes/cee-prs-small-dd2.smt2
   regress1/datatypes/dt-color-2.6.smt2

diff --git a/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 b/test/regress/regress1/arith/issue6774-sanity-int-model.smt2
new file mode 100644 (file)
index 0000000..732b709
--- /dev/null
+++ b/test/regress/regress1/arith/issue6774-sanity-int-model.smt2
@@ -0,0 +1,21 @@
+; COMMAND-LINE: -i -q
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALIRA)
+(declare-const x Real)
+(declare-fun i () Int)
+(declare-fun i1 () Int)
+(push)
+(assert (< 1 (- i)))
+(check-sat)
+(pop)
+(push)
+(assert (or (>= i1 (* 5 (- i)))))
+(check-sat)
+(pop)
+(assert (or (> i1 1) (= x (to_real i))))
+(check-sat)
+(assert (not (is_int x)))
+(check-sat)

diff --git a/test/regress/regress1/arith/issue7252-arith-sanity.smt2 b/test/regress/regress1/arith/issue7252-arith-sanity.smt2
new file mode 100644 (file)
index 0000000..dd7a1fa
--- /dev/null
+++ b/test/regress/regress1/arith/issue7252-arith-sanity.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(declare-fun d () Int)
+(declare-fun e () Int)
+(declare-fun f () Int)
+(declare-fun g () Int)
+(assert (> 0 (* a (mod 0 b))))
+(assert (or (and (> (* b d) (* 2 (+ g c))) (= g (- c)) (> (+ e c) 0)) (> f 0)))
+(check-sat)

diff --git a/test/regress/regress1/cores/issue6988-arith-sanity.smt2 b/test/regress/regress1/cores/issue6988-arith-sanity.smt2
new file mode 100644 (file)
index 0000000..622d643
--- /dev/null
+++ b/test/regress/regress1/cores/issue6988-arith-sanity.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: -i -q
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ANIA)
+(declare-const x Bool)
+(set-option :produce-unsat-cores true)
+(declare-fun i () Int)
+(declare-fun i5 () Int)
+(declare-fun i8 () Int)
+(assert (or x (< i5 0)))
+(push)
+(assert (and (= i8 1) (= i5 (+ 1 i)) (= i8 (+ 1 i))))
+(push)
+(check-sat)
+(pop)
+(pop)
+(assert (= i8 (* i8 3 (+ i8 1))))
+(check-sat)