Use SAT context level for --bv-assert-input instead of decision level. (#6758)
authorMathias Preiner <mathias.preiner@gmail.com>
Wed, 30 Jun 2021 22:07:47 +0000 (15:07 -0700)
committerGitHub <noreply@github.com>
Wed, 30 Jun 2021 22:07:47 +0000 (22:07 +0000)
commitd288f52dd82fe6590950758289e86ebcb039350d
treef025c84989cc7e096ae365b9671bef267da546c8
parent46c994963ef764101409d55d77e0e15db704827b
Use SAT context level for --bv-assert-input instead of decision level. (#6758)

The decision level as previously implemented was not accurate since it
did not consider the user context level. This resulted in facts being
incorrectly recognized as input assertions, which happened for
incremental benchmarks.
src/prop/minisat/minisat.cpp
src/prop/minisat/minisat.h
src/prop/prop_engine.h
src/theory/bv/bv_solver_bitblast.cpp
src/theory/valuation.h
test/regress/CMakeLists.txt
test/regress/regress0/issue6738.smt2 [new file with mode: 0644]