Few regression tests on unsat cores with more possibilities

test/regression/base/generic/redundant_unsat_core.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 (! (not b1) :named a3))
+(assert (! (and b1 b2) :named x1))
+(assert (! (or b1 b2) :named x2))
+(assert (! (xor b1 b2) :named x3))
+
+(check-sat)
+(get-unsat-core)

test/regression/base/generic/redundant_unsat_core.smt2.expected.out

@@ -0,0 +1,2 @@
+unsat
+( a1 a3 )

test/regression/base/generic/redundant_unsat_core2.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) :named x1))
+(assert (! (or b1 b2) :named x2))
+(assert (! (xor b1 b2) :named x3))
+(assert (! b1 :named a1))
+(assert (! b2 :named a2))
+(assert (! (not b1) :named a3))
+
+(check-sat)
+(get-unsat-core)

test/regression/base/generic/redundant_unsat_core2.smt2.expected.out

@@ -0,0 +1,2 @@
+unsat
+( x1 x3 )

test/regression/base/generic/redundant_unsat_core3.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))
+(assert (xor b1 b2))
+(assert (! b1 :named a1))
+(assert (! b2 :named a2))
+(assert (! (not b1) :named a3))
+
+(check-sat)
+(get-unsat-core)

test/regression/base/generic/redundant_unsat_core3.smt2.expected.out

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