diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-07-14 19:39:00 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-15 02:39:00 +0000 |
| commit | d3fafcf6d7881eea61f22141b8b8feb2cdcee1f7 (patch) | |
| tree | 04350ed157c1459a2109f972941e6678e2d26e95 | |
| parent | d7bb2484436a55c6b2df08bcae7549809e3ad264 (diff) | |
bv: Disable bv-assert-input if proofs are enabled. (#6886)
| -rw-r--r-- | src/smt/set_defaults.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
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 = |