summaryrefslogtreecommitdiff
path: root/test/system/CVC4JavaTest.java
diff options
context:
space:
mode:
authorAndres Notzli <andres.noetzli@gmail.com>2016-12-14 21:20:17 -0800
committerAndres Notzli <andres.noetzli@gmail.com>2016-12-16 17:00:05 -0800
commit59c6247bc8b0c9518abbacffa9ba400d4e5a6689 (patch)
tree4ae17aa18bc3370925044ee935057e9b3e449852 /test/system/CVC4JavaTest.java
parent67fd8cc104ec9861ca234bb3170c7f992eea3868 (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/system/CVC4JavaTest.java')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback