diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-16 10:37:19 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-16 10:37:19 -0700 |
| commit | 33f77f7e95575cbaf5249042fa83d7b0d0650ce0 (patch) | |
| tree | 985a074d0cec25a6eadbbb1c7621d1a9bacc1b4d /test/regress/regress0 | |
| parent | 227cd8c26c508b7b444fbed6f2868f90c8281eed (diff) | |
Create master equality engine at context level 0 (#4081)
Fixes #4077. The master equality engine in `TheoryEngine` was being
created at SAT context level 1. If the context was popped to level zero
by `(reset-assertions)`, `true` and `false` were removed from the master
equality engine, which lead for example to `(= ((_ extract 3 3) x) (_
bv1 1))` and `(_ bv1 4)` being merged (this can be gathered from looking
at `-t equality`). This commit fixes the issue by postponing the global
context pushes until after the theory engine has been initialized.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/smtlib/issue4077.smt2 | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test/regress/regress0/smtlib/issue4077.smt2 b/test/regress/regress0/smtlib/issue4077.smt2 new file mode 100644 index 000000000..76a37886b --- /dev/null +++ b/test/regress/regress0/smtlib/issue4077.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat + +; Use a quantified logic to make sure that TheoryEngine creates a master +; equality engine +(set-logic BV) +(declare-const x (_ BitVec 4)) +(push) +(reset-assertions) +(assert (bvslt (bvsrem (_ bv1 4) x) (_ bv1 4))) +(check-sat) |