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/prop/prop_engine.h | |
| 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/prop/prop_engine.h')
| -rw-r--r-- | src/prop/prop_engine.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 74da49cf6..e458ca5e5 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -157,7 +157,7 @@ class PropEngine bool isDecision(Node lit) const; /** - * Return the current decision level of `lit`. + * Return SAT context level at which `lit` was decided on. * * @param lit: The node in question, must have an associated SAT literal. * @return Decision level of the SAT variable of `lit` (phase is disregarded), |