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.

diff --git a/src/smt/ite_removal.cpp b/src/smt/ite_removal.cpp
index fcd0c325437ef169236dce5f196b717bf3ba9b13..d31d541212e6d7c5005d59858b3c77d05b9a7f1b 100644 (file)
--- a/src/smt/ite_removal.cpp
+++ b/src/smt/ite_removal.cpp
@@ -17,6 +17,7 @@
 
 #include <vector>
 
+#include "options/proof_options.h"
 #include "proof/proof_manager.h"
 #include "theory/ite_utilities.h"
 
@@ -55,7 +56,8 @@ void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool
     // fixes the bug on clang on Mac OS
     Node itesRemoved = run(output[i], output, iteSkolemMap, false);
     // In some calling contexts, not necessary to report dependence information.
-    if(reportDeps && options::unsatCores()) {
+    if (reportDeps &&
+        (options::unsatCores() || options::fewerPreprocessingHoles())) {
       // new assertions have a dependence on the node
       PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); )
       while(n < output.size()) {

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 5ef768fd3ed2057a30bb29c9c179468ea27b8831..8da1dfc1bbf9581585703906c4962c52d083afbb 100644 (file)
--- 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;

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index bb5c1e5878a34e8fcf913be2f9295218d6ba427d..0c49af3069aa5e8288905e4ce1c312b7eabde495 100644 (file)
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -100,7 +100,8 @@ SMT_TESTS = \
        bv2nat-simp-range.smt2 \
        bv-int-collapse1.smt2 \
        bv-int-collapse2.smt2 \
-       bv-int-collapse2-sat.smt2
+       bv-int-collapse2-sat.smt2 \
+       bench_38.delta.smt2
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS = divtest.smt2

diff --git a/test/regress/regress0/bv/bench_38.delta.smt2 b/test/regress/regress0/bv/bench_38.delta.smt2
new file mode 100644 (file)
index 0000000..7606143
--- /dev/null
+++ b/test/regress/regress0/bv/bench_38.delta.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --fewer-preprocessing-holes --check-proof --quiet
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun x () (_ BitVec 4))
+(assert (and (= (bvudiv (_ bv2 4) x) (_ bv2 4)) (= (_ bv0 4) x) (= (_ bv1 4) x)))
+(check-sat)
+(exit)