Create master equality engine at context level 0 (#4081)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 16 Mar 2020 17:37:19 +0000 (10:37 -0700)
committerGitHub <noreply@github.com>
Mon, 16 Mar 2020 17:37:19 +0000 (10:37 -0700)
commit33f77f7e95575cbaf5249042fa83d7b0d0650ce0
tree985a074d0cec25a6eadbbb1c7621d1a9bacc1b4d
parent227cd8c26c508b7b444fbed6f2868f90c8281eed
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.
src/smt/smt_engine.cpp
src/theory/uf/equality_engine.cpp
test/regress/CMakeLists.txt
test/regress/regress0/smtlib/issue4077.smt2 [new file with mode: 0644]
test/unit/theory/theory_arith_white.h