From 4ac14c09322f234ba2a201e0d281664338fd9ee0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 28 Feb 2020 22:30:40 -0600 Subject: 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. --- src/theory/theory_model_builder.cpp | 5 ++--- test/regress/CMakeLists.txt | 1 + test/regress/regress0/arrays/issue3813-massign-assert.smt2 | 8 ++++++++ 3 files changed, 11 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/arrays/issue3813-massign-assert.smt2 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) -- cgit v1.2.3