More fixes for quantifier elimination (#5533)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 1 Dec 2020 04:22:24 +0000 (22:22 -0600)
committerGitHub <noreply@github.com>
Tue, 1 Dec 2020 04:22:24 +0000 (22:22 -0600)
commit6489cf590b441aeb5e1bdf9800c9718d06842149
tree98eaa6adb49fea33593a770d37d2e89cc7c15bbb
parentacdffc72bd559fa4b64da2ee2b3373208354e7a1
More fixes for quantifier elimination (#5533)

Fixes #5506, fixes #5507.
src/smt/quant_elim_solver.cpp
src/smt/quant_elim_solver.h
src/smt/smt_engine.cpp
src/theory/quantifiers_engine.cpp
test/regress/CMakeLists.txt
test/regress/regress1/quantifiers/issue5506-qe.smt2 [new file with mode: 0644]
test/regress/regress1/quantifiers/issue5507-qe.smt2 [new file with mode: 0644]