Added also other orders and namings of "redundant" unsat-core regress…

…ion tests

test/regression/unsatcores/generic/redundant-even-named-mix.smt2

@@ -0,0 +1,16 @@
+(set-option :produce-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert b1)
+(assert (! b2 :named a2))
+(assert (and b1 b2))
+(assert (! (or b1 b2) :named x2))
+(assert (not b1))
+(assert (! (xor b1 b2) :named x3))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-even-named-mix.smt2.expected.out

@@ -0,0 +1,3 @@
+unsat
+(
+)

test/regression/unsatcores/generic/redundant-even-named-mix_min.smt2

@@ -0,0 +1,17 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert b1)
+(assert (! b2 :named a2))
+(assert (and b1 b2))
+(assert (! (or b1 b2) :named x2))
+(assert (not b1))
+(assert (! (xor b1 b2) :named x3))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-even-named-mix_min.smt2.expected.out

@@ -0,0 +1,3 @@
+unsat
+(
+)

test/regression/unsatcores/generic/redundant-even-named-swap.smt2

@@ -0,0 +1,16 @@
+(set-option :produce-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert (and b1 b2))
+(assert (! (or b1 b2) :named x2))
+(assert (xor b1 b2))
+(assert (! b1 :named a1))
+(assert b2)
+(assert (! (not b1) :named a3))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-even-named-swap.smt2.expected.out

@@ -0,0 +1,3 @@
+unsat
+(
+)

test/regression/unsatcores/generic/redundant-even-named-swap_full.smt2

@@ -0,0 +1,17 @@
+(set-option :produce-unsat-cores true)
+(set-option :print-cores-full true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert (and b1 b2))
+(assert (! (or b1 b2) :named x2))
+(assert (xor b1 b2))
+(assert (! b1 :named a1))
+(assert b2)
+(assert (! (not b1) :named a3))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-even-named-swap_full.smt2.expected.out

@@ -0,0 +1,5 @@
+unsat
+(
+(and b1 b2)
+(xor b1 b2)
+)

test/regression/unsatcores/generic/redundant-even-named-swap_min.smt2

@@ -0,0 +1,17 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert (and b1 b2))
+(assert (! (or b1 b2) :named x2))
+(assert (xor b1 b2))
+(assert (! b1 :named a1))
+(assert b2)
+(assert (! (not b1) :named a3))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-even-named-swap_min.smt2.expected.out

@@ -0,0 +1,3 @@
+unsat
+(
+)

test/regression/unsatcores/generic/redundant-even-named-swap_min_full.smt2

@@ -0,0 +1,18 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+(set-option :print-cores-full true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert (and b1 b2))
+(assert (! (or b1 b2) :named x2))
+(assert (xor b1 b2))
+(assert (! b1 :named a1))
+(assert b2)
+(assert (! (not b1) :named a3))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-even-named-swap_min_full.smt2.expected.out

@@ -0,0 +1,5 @@
+unsat
+(
+(and b1 b2)
+(xor b1 b2)
+)

test/regression/unsatcores/generic/redundant-even-named.smt2

@@ -0,0 +1,16 @@
+(set-option :produce-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert b1)
+(assert (! b2 :named a2))
+(assert (not b1))
+(assert (! (and b1 b2) :named x1))
+(assert (or b1 b2))
+(assert (! (xor b1 b2) :named x3))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-even-named.smt2.expected.out

@@ -0,0 +1,3 @@
+unsat
+(
+)

test/regression/unsatcores/generic/redundant-even-named_full.smt2

@@ -0,0 +1,17 @@
+(set-option :produce-unsat-cores true)
+(set-option :print-cores-full true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert b1)
+(assert (! b2 :named a2))
+(assert (not b1))
+(assert (! (and b1 b2) :named x1))
+(assert (or b1 b2))
+(assert (! (xor b1 b2) :named x3))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-even-named_full.smt2.expected.out

@@ -0,0 +1,5 @@
+unsat
+(
+b1
+(not b1)
+)

test/regression/unsatcores/generic/redundant-even-named_min.smt2

@@ -0,0 +1,17 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert b1)
+(assert (! b2 :named a2))
+(assert (not b1))
+(assert (! (and b1 b2) :named x1))
+(assert (or b1 b2))
+(assert (! (xor b1 b2) :named x3))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-even-named_min.smt2.expected.out

@@ -0,0 +1,3 @@
+unsat
+(
+)

test/regression/unsatcores/generic/redundant-even-named_min_full.smt2

@@ -0,0 +1,18 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+(set-option :print-cores-full true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert b1)
+(assert (! b2 :named a2))
+(assert (not b1))
+(assert (! (and b1 b2) :named x1))
+(assert (or b1 b2))
+(assert (! (xor b1 b2) :named x3))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-even-named_min_full.smt2.expected.out

@@ -0,0 +1,5 @@
+unsat
+(
+b1
+(not b1)
+)

test/regression/unsatcores/generic/redundant-half1-named-mix.smt2

@@ -0,0 +1,16 @@
+(set-option :produce-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert (! b1 :named a1))
+(assert (! b2 :named a2))
+(assert (! (and b1 b2) :named x1))
+(assert (or b1 b2))
+(assert (not b1))
+(assert (xor b1 b2))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-half1-named-mix.smt2.expected.out

@@ -0,0 +1,4 @@
+unsat
+(
+a1
+)

test/regression/unsatcores/generic/redundant-half1-named-mix_min.smt2

@@ -0,0 +1,17 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert (! b1 :named a1))
+(assert (! b2 :named a2))
+(assert (! (and b1 b2) :named x1))
+(assert (or b1 b2))
+(assert (not b1))
+(assert (xor b1 b2))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-half1-named-mix_min.smt2.expected.out

@@ -0,0 +1,4 @@
+unsat
+(
+a1
+)

test/regression/unsatcores/generic/redundant-half2-named-mix.smt2

@@ -0,0 +1,16 @@
+(set-option :produce-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert b1)
+(assert b2)
+(assert (and b1 b2))
+(assert (! (or b1 b2) :named x2))
+(assert (! (not b1) :named a3))
+(assert (! (xor b1 b2) :named x3))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-half2-named-mix.smt2.expected.out

@@ -0,0 +1,4 @@
+unsat
+(
+a3
+)

test/regression/unsatcores/generic/redundant-half2-named-mix_min.smt2

@@ -0,0 +1,17 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert b1)
+(assert b2)
+(assert (and b1 b2))
+(assert (! (or b1 b2) :named x2))
+(assert (! (not b1) :named a3))
+(assert (! (xor b1 b2) :named x3))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-half2-named-mix_min.smt2.expected.out

@@ -0,0 +1,4 @@
+unsat
+(
+a3
+)

test/regression/unsatcores/generic/redundant-mix.smt2

@@ -0,0 +1,16 @@
+(set-option :produce-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert b1)
+(assert b2)
+(assert (not b1))
+(assert (and b1 b2))
+(assert (or b1 b2))
+(assert (xor b1 b2))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-mix.smt2.expected.out

@@ -0,0 +1,3 @@
+unsat
+(
+)

test/regression/unsatcores/generic/redundant-mix_full.smt2

@@ -0,0 +1,17 @@
+(set-option :produce-unsat-cores true)
+(set-option :print-cores-full true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert b1)
+(assert b2)
+(assert (not b1))
+(assert (and b1 b2))
+(assert (or b1 b2))
+(assert (xor b1 b2))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-mix_full.smt2.expected.out

@@ -0,0 +1,5 @@
+unsat
+(
+b1
+(not b1)
+)

test/regression/unsatcores/generic/redundant-mix_min.smt2

@@ -0,0 +1,17 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert b1)
+(assert b2)
+(assert (not b1))
+(assert (and b1 b2))
+(assert (or b1 b2))
+(assert (xor b1 b2))
+
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/generic/redundant-mix_min.smt2.expected.out

@@ -0,0 +1,3 @@
+unsat
+(
+)