diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-28 22:30:40 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-28 20:30:40 -0800 |
| commit | 4ac14c09322f234ba2a201e0d281664338fd9ee0 (patch) | |
| tree | 842c67e61698fac5a82125c65ad77b049bc9349f | |
| parent | 940a25255469bbeea95df14ef25036e6c0565c3e (diff) | |
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.
| -rw-r--r-- | src/theory/theory_model_builder.cpp | 5 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/arrays/issue3813-massign-assert.smt2 | 8 |
3 files changed, 11 insertions, 3 deletions
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index e15211847..a96f29ada 100644 --- 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 32ee2a744..d273b768d 100644 --- 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 index 000000000..7de7aebc8 --- /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) |