From: Andres Notzli <andres.noetzli@gmail.com>
Date: Thu, 15 Dec 2016 05:20:17 +0000 (-0800)
Subject: Fix dependency tracing for fewerPreprocessingHoles
X-Git-Tag: cvc5-1.0.0~5930^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=59c6247bc8b0c9518abbacffa9ba400d4e5a6689;p=cvc5.git

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 fcd0c3254..d31d54121 100644
--- 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 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;
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index bb5c1e587..0c49af306 100644
--- 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
index 000000000..760614348
--- /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)