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 f4d885f4b966e5c85e146f43e548eb4a8a0d9463..bb104e98d41c8d2d8e1fe1d4c9ab58a4502bcadd 100644 (file)
--- 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 =