From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Thu, 15 Jul 2021 02:39:00 +0000 (-0700)
Subject: bv: Disable bv-assert-input if proofs are enabled. (#6886)
X-Git-Tag: cvc5-1.0.0~1482
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d3fafcf6d7881eea61f22141b8b8feb2cdcee1f7;p=cvc5.git

bv: Disable bv-assert-input if proofs are enabled. (#6886)
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index f4d885f4b..bb104e98d 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -404,6 +404,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.smt.produceAssertions = true;
   }
 
+  if (options::bvAssertInput() && options::produceProofs())
+  {
+    Notice() << "Disabling bv-assert-input since it is incompatible with proofs."
+             << std::endl;
+    opts.bv.bvAssertInput = false;
+  }
+
   // whether we want to force safe unsat cores, i.e., if we are in the default
   // ASSUMPTIONS mode, since other ones are experimental
   bool safeUnsatCores =