Fix assertion related to assignability in the model. (#3843)

Fixes #3813.

It appears that an assertion was hardcoded to check whether a term was a variable or APPLY_UF application whereas this check should use isAssignable. This avoids an assertion failure on the given benchmark.

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index e15211847170d34c24c25a1683ae0a3186a706de..a96f29ada76cca8df866e23fce1fc97162d6b9f0 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -788,13 +788,12 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
         {
           Assert(!evaluable || assignOne);
           // this assertion ensures that if we are assigning to a term of
-          // Boolean type, then the term is either a variable or an APPLY_UF.
+          // Boolean type, then the term must be assignable.
           // Note we only assign to terms of Boolean type if the term occurs in
           // a singleton equivalence class; otherwise the term would have been
           // in the equivalence class of true or false and would not need
           // assigning.
-          Assert(!t.isBoolean() || (*i2).isVar()
-                 || (*i2).getKind() == kind::APPLY_UF);
+          Assert(!t.isBoolean() || isAssignable(*i2));
           Node n;
           if (itAssigner != eqcToAssigner.end())
           {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 32ee2a744996099ffad745b1ed8a6191dd51f4ad..d273b768d4bec75eae217089cf40c11cd7d3846f 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -75,6 +75,7 @@ set(regress_0_tests
   regress0/arrays/incorrect8.minimized.smtv1.smt2
   regress0/arrays/incorrect8.smtv1.smt2
   regress0/arrays/incorrect9.smtv1.smt2
+  regress0/arrays/issue3813-massign-assert.smt2
   regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2
   regress0/arrays/x2.smtv1.smt2
   regress0/arrays/x3.smtv1.smt2

diff --git a/test/regress/regress0/arrays/issue3813-massign-assert.smt2 b/test/regress/regress0/arrays/issue3813-massign-assert.smt2
new file mode 100644 (file)
index 0000000..7de7aeb
--- /dev/null
+++ b/test/regress/regress0/arrays/issue3813-massign-assert.smt2
@@ -0,0 +1,8 @@
+; EXPECT: sat
+; COMMAND-LINE: --check-unsat-cores
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Array Int Bool))
+(declare-fun b () (Array Int Bool))
+(assert (= a (store b 0 true)))
+(check-sat)