Fix dependency tracing for fewerPreprocessingHoles
authorAndres Notzli <andres.noetzli@gmail.com>
Thu, 15 Dec 2016 05:20:17 +0000 (21:20 -0800)
committerAndres Notzli <andres.noetzli@gmail.com>
Sat, 17 Dec 2016 01:00:05 +0000 (17:00 -0800)
commit59c6247bc8b0c9518abbacffa9ba400d4e5a6689
tree4ae17aa18bc3370925044ee935057e9b3e449852
parent67fd8cc104ec9861ca234bb3170c7f992eea3868
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.
src/smt/ite_removal.cpp
src/theory/theory_engine.cpp
test/regress/regress0/bv/Makefile.am
test/regress/regress0/bv/bench_38.delta.smt2 [new file with mode: 0644]