diff options
| author | guykatzz <guyk@cs.stanford.edu> | 2017-01-04 10:18:36 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-01-04 10:18:36 -0800 |
| commit | 8c99adc0fab8e482023750628431fe28ef49438b (patch) | |
| tree | b9663783aae48bb7d40ab6faa2d6e3092954167d /src/theory | |
| parent | 7c10e3b927c4f7b4cf2ae285cc8f9485e2616db6 (diff) | |
| parent | 59c6247bc8b0c9518abbacffa9ba400d4e5a6689 (diff) | |
Merge pull request #120 from 4tXJ7f/fix_f_pp_holes
Fix dependency tracing for fewerPreprocessingHoles
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/theory_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5ef768fd3..8da1dfc1b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -25,6 +25,7 @@ #include "expr/node_builder.h" #include "options/bv_options.h" #include "options/options.h" +#include "options/proof_options.h" #include "options/quantifiers_options.h" #include "proof/cnf_proof.h" #include "proof/lemma_proof.h" @@ -1945,7 +1946,7 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){ // This pass does not support dependency tracking yet // (learns substitutions from all assertions so just // adding addDependence is not enough) - if (options::unsatCores()) { + if (options::unsatCores() || options::fewerPreprocessingHoles()) { return true; } bool result = true; |