Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv-ineq when proofs are enabled (#1801)

Currently, if the user enables proofs but does not disable the algebraic/equality/inequality bv-solvers, then we reach an internal error while printing the proof (unreachable code becomes reachable).
This commit auto-disable these bv options when proofs are enabled, unless these options were set by the user. In such a case, an error message is given to the user.

4 files changed, 96 insertions, 0 deletions

diff --git a/test/regress/regress0/bv/bv-options1.smt2 b/test/regress/regress0/bv/bv-options1.smt2
new file mode 100644
index 000000000..b1e87fc7e
--- /dev/null
+++ b/test/regress/regress0/bv/bv-options1.smt2
@@ -0,0 +1,24 @@
+; SCRUBBER: sed -e 's/(error \"Error.in.option.parsing.*$/Error in option parsing/'
+; EXPECT: Error in option parsing
+; COMMAND-LINE: --check-proofs --bv-algebraic-solver
+; EXIT: 1
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(declare-fun v0 () (_ BitVec 16))
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun v2 () (_ BitVec 16))
+(declare-fun v3 () (_ BitVec 16))
+(declare-fun v4 () (_ BitVec 16))
+(declare-fun v5 () (_ BitVec 16))
+(assert (and
+	 (bvult v2 v4)
+	 (bvult v3 v4)
+	 (bvult v0 v1)
+	 (bvult v1 v2)
+	 (bvult v1 v3)
+	 (bvult v4 v5)
+	 (bvult v5 v1)
+	 ))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/bv-options2.smt2 b/test/regress/regress0/bv/bv-options2.smt2
new file mode 100644
index 000000000..d1ee44084
--- /dev/null
+++ b/test/regress/regress0/bv/bv-options2.smt2
@@ -0,0 +1,24 @@
+; SCRUBBER: sed -e 's/(error \"Error.in.option.parsing.*$/Error in option parsing/'
+; EXPECT: Error in option parsing
+; COMMAND-LINE: --check-proofs --bv-eq-solver
+; EXIT: 1
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(declare-fun v0 () (_ BitVec 16))
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun v2 () (_ BitVec 16))
+(declare-fun v3 () (_ BitVec 16))
+(declare-fun v4 () (_ BitVec 16))
+(declare-fun v5 () (_ BitVec 16))
+(assert (and
+	 (bvult v2 v4)
+	 (bvult v3 v4)
+	 (bvult v0 v1)
+	 (bvult v1 v2)
+	 (bvult v1 v3)
+	 (bvult v4 v5)
+	 (bvult v5 v1)
+	 ))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/bv-options3.smt2 b/test/regress/regress0/bv/bv-options3.smt2
new file mode 100644
index 000000000..4d16230b4
--- /dev/null
+++ b/test/regress/regress0/bv/bv-options3.smt2
@@ -0,0 +1,24 @@
+; SCRUBBER: sed -e 's/(error \"Error.in.option.parsing.*$/Error in option parsing/'
+; EXPECT: Error in option parsing
+; COMMAND-LINE: --check-proofs --bv-inequality-solver
+; EXIT: 1
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(declare-fun v0 () (_ BitVec 16))
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun v2 () (_ BitVec 16))
+(declare-fun v3 () (_ BitVec 16))
+(declare-fun v4 () (_ BitVec 16))
+(declare-fun v5 () (_ BitVec 16))
+(assert (and
+	 (bvult v2 v4)
+	 (bvult v3 v4)
+	 (bvult v0 v1)
+	 (bvult v1 v2)
+	 (bvult v1 v3)
+	 (bvult v4 v5)
+	 (bvult v5 v1)
+	 ))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/bv-options4.smt2 b/test/regress/regress0/bv/bv-options4.smt2
new file mode 100644
index 000000000..842650ebd
--- /dev/null
+++ b/test/regress/regress0/bv/bv-options4.smt2
@@ -0,0 +1,24 @@
+; SCRUBBER: sed -e 's/unsat.*/unsat/'
+; EXPECT: unsat
+; COMMAND-LINE: --check-proofs 
+; EXIT: 0
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(declare-fun v0 () (_ BitVec 16))
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun v2 () (_ BitVec 16))
+(declare-fun v3 () (_ BitVec 16))
+(declare-fun v4 () (_ BitVec 16))
+(declare-fun v5 () (_ BitVec 16))
+(assert (and
+	 (bvult v2 v4)
+	 (bvult v3 v4)
+	 (bvult v0 v1)
+	 (bvult v1 v2)
+	 (bvult v1 v3)
+	 (bvult v4 v5)
+	 (bvult v5 v1)
+	 ))
+(check-sat)
+(exit)