From d3fafcf6d7881eea61f22141b8b8feb2cdcee1f7 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 14 Jul 2021 19:39:00 -0700 Subject: [PATCH] bv: Disable bv-assert-input if proofs are enabled. (#6886) --- src/smt/set_defaults.cpp | 7 +++++++ 1 file changed, 7 insertions(+) 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 = -- 2.30.2