diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-06-30 15:07:47 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-30 22:07:47 +0000 |
| commit | d288f52dd82fe6590950758289e86ebcb039350d (patch) | |
| tree | f025c84989cc7e096ae365b9671bef267da546c8 /src/theory/bv/bv_solver_bitblast.cpp | |
| parent | 46c994963ef764101409d55d77e0e15db704827b (diff) | |
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.
Diffstat (limited to 'src/theory/bv/bv_solver_bitblast.cpp')
| -rw-r--r-- | src/theory/bv/bv_solver_bitblast.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index 3ae4a7f0a..a5d89e371 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -219,9 +219,9 @@ bool BVSolverBitblast::preNotifyFact( * using assumptions. */ if (options::bvAssertInput() && val.isSatLiteral(fact) - && !val.isDecision(fact) && val.getDecisionLevel(fact) == 0 - && val.getIntroLevel(fact) == 0) + && val.getDecisionLevel(fact) == 0 && val.getIntroLevel(fact) == 0) { + Assert(!val.isDecision(fact)); d_bbInputFacts.push_back(fact); } else |