diff options
author | Andres Notzli <andres.noetzli@gmail.com> | 2016-12-14 21:20:17 -0800 |
---|---|---|
committer | Andres Notzli <andres.noetzli@gmail.com> | 2016-12-16 17:00:05 -0800 |
commit | 59c6247bc8b0c9518abbacffa9ba400d4e5a6689 (patch) | |
tree | 4ae17aa18bc3370925044ee935057e9b3e449852 /test/regress/regress0/bug274.cvc | |
parent | 67fd8cc104ec9861ca234bb3170c7f992eea3868 (diff) |
Fix dependency tracing for fewerPreprocessingHoles
Previously, dependency tracing in `ite_removal.cpp` was only done with
the `unsatCores` option but `fewerPreprocessingHoles` requires
dependencies, too. This lead to errors during proof construction when
`fewerPreprocessingHoles` was active. This commit fixes the condition
and includes a test case that previously failed. Additionally, it fixes
a similar issue in the theory engine.
NOTE: this commit might not fix all instances of this problem.
`smt_engine.cpp` turns certain flags off with `unsatCores`.
Compatibility between those flags and `fewerPreprocessingHoles` needs to
be checked separately.
Diffstat (limited to 'test/regress/regress0/bug274.cvc')
0 files changed, 0 insertions, 0 deletions