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 /test | |
| 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.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/arrays/issue3813-massign-assert.smt2 | 8 |
2 files changed, 9 insertions, 0 deletions
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) |