Regression tests on unsat cores with terms that may internally be changed

Author: Tomaqa

test/regression/unsatcores/QF_LIA/calypto-1.smt2

@@ -0,0 +1,26 @@
+(set-option :produce-unsat-cores true)
+(set-logic QF_LIA)
+(declare-fun x83 () Bool)
+(declare-fun x60 () Bool)
+(declare-fun x113 () Bool)
+(declare-fun x58 () Bool)
+(declare-fun x51 () Bool)
+(declare-fun x65 () Bool)
+(declare-fun x46 () Bool)
+(declare-fun x5 () Bool)
+(declare-fun x59 () Bool)
+(declare-fun x138 () Bool)
+(declare-fun x95 () Bool)
+(declare-fun x54 () Bool)
+(declare-fun x62 () Bool)
+(declare-fun x112 () Bool)
+(declare-fun x9 () Bool)
+(declare-fun x116 () Int)
+(declare-fun x49 () Bool)
+(declare-fun x40 () Int)
+(assert (! (let ((x66 (ite (not x62) x138 false)) (x21 (not x54)) (x26 (not x59))) (let ((x19 (ite x26 (ite x21 x66 true) x66)) (x2 (not x113))) (let ((x64 (not (not x19))) (x50 (ite x2 true false)) (x89 (not x51))) (let ((x82 (ite x64 false (ite x89 x50 true))) (x13 (not x95))) (let ((x80 (ite x13 true false)) (x130 (not x82)) (x121 (not x46))) (let ((x125 (ite x66 1 0)) (x36 (not x66)) (x110 (ite x130 false (ite x121 x80 true)))) (let ((x7 (+ 1 x125))) (let ((x88 (ite x64 x7 (ite (ite x89 (ite x2 x66 false) x66) 1 0)))) (let ((x17 (+ x88 1))) (let ((x102 (ite x130 x17 (ite x121 (ite x13 x88 0) x88)))) (let ((x119 (not x110)) (x123 (+ 1 x102)) (x61 (not x36)) (x37 (not x83)) (x108 (not x5))) (let ((x15 (ite x119 (ite x61 (ite x108 (ite x37 x123 0) x123) x123) (ite x108 (ite x37 x102 0) x102)))) (let ((x107 (+ x15 1))) (let ((x124 (= 2 x107)) (x33 (= x123 2)) (x133 (ite x37 true false))) (let ((x104 (ite x108 x133 true))) (let ((x56 (not x9)) (x8 (ite x119 (ite x61 x104 false) x104))) (let ((x44 (not x60)) (x106 (ite x56 true false))) (let ((x72 (ite x44 x106 true)) (x30 (not x8)) (x32 (not (> 4 x107)))) (let ((x137 (ite x30 (ite x32 x72 false) x72))) (let ((x115 (or (ite x44 (ite x108 (ite x121 (ite x89 (ite x26 x66 false) false) false) false) false) x112)) (x10 (not (or x137 x33))) (x43 (not x65))) (let ((x39 (or (or x10 x115) x65))) (let ((x79 (= 2 x17)) (x122 (not (or (ite x43 (ite x44 (ite x108 (ite x121 (ite x89 (ite x26 x54 false) false) false) false) false) false) x49))) (x63 (not x39)) (x12 (not x115))) (let ((x45 (not (or x79 x8))) (x78 (and x119 x36))) (let ((x28 (and (not x78) (or x78 (not (ite x108 x83 false)))))) (let ((x100 (not x28))) (let ((x29 (and (not x79) x100))) (let ((x68 (not x29))) (let ((x105 (and (or (not (ite x44 x9 false)) x45) x68))) (let ((x134 (not x105))) (let ((x135 (and (not x33) x134))) (let ((x118 (not x135))) (let ((x129 (not x124)) (x23 (and (or (or x65 x12) x10) x118))) (let ((x67 (and x129 (not x23)))) (let ((x93 (ite x21 x125 x7)) (x57 (not x67)) (x114 (not x49))) (let ((x3 (ite x61 x93 (ite x26 x93 0)))) (let ((x42 (ite x2 x3 (+ x3 1)))) (let ((x117 (ite x64 x42 (ite x89 x42 0)))) (let ((x98 (ite x13 x117 (+ x117 1)))) (let ((x127 (ite x130 x98 (ite x121 x98 0)))) (let ((x47 (ite x37 x127 (+ 1 x127)))) (let ((x31 (ite x108 x47 0))) (let ((x1 (ite x119 (ite x61 x31 x47) x31))) (let ((x91 (ite x56 x1 (+ x1 1)))) (let ((x14 (ite x44 x91 0))) (let ((x131 (ite x30 (ite x32 x14 x91) x14))) (let ((x4 (not (ite x61 (ite x21 x66 false) x19))) (x109 (< (ite (< x131 4) x131 (- x131 8)) 0)) (x86 (not (or x50 x82)))) (let ((x71 (not (or (not (or x86 x4)) (and x86 x4))))) (let ((x25 (or (not (or x71 (not (and x80 x119)))) (and (not (or x80 x110)) x71)))) (let ((x84 (not x25)) (x74 (not (or x78 x108)))) (let ((x140 (or (or (not (or (not (and x133 x100)) x84)) (and x25 x74)) (and x84 (not (or x133 x28))))) (x126 (not (or x5 (or x78 x83))))) (let ((x101 (not (and (not (and x140 x79)) (not (and x126 (and x66 x25))))))) (let ((x136 (and (not (and x29 x140)) (not (and x101 x68))))) (let ((x97 (not (or x133 x84))) (x55 (not (or x71 x80))) (x6 (not (or (not (or x21 x36)) (not (or x50 x4))))) (x120 (not (or x106 x136)))) (let ((x76 (or (not (or x55 x6)) (and x55 x6)))) (let ((x18 (not x76))) (let ((x52 (not (and (or (not (or (and x18 x97) (not (or x18 x97)))) x28) (not (and x74 x76))))) (x35 (and (and x76 x66) x126))) (let ((x96 (not (and (not (and x35 x126)) (not (and x79 x52)))))) (let ((x69 (or x60 (or x45 x9))) (x75 (and (not (and x96 x68)) (not (and x29 x52))))) (let ((x85 (and x105 x69))) (let ((x73 (or x105 x106)) (x38 (not (and (not (and x52 x85)) (or (not (or (and x75 x120) (not (or x120 x75)))) x105)))) (x16 (not x69))) (let ((x22 (not x112)) (x48 (or (and x136 (not x73)) (or (not (or (not (and x106 x134)) x136)) (and x140 x85))))) (let ((x20 (and (not (or (and (not (and (not (and (not (and x33 x48)) (not (and x101 x16)))) x118)) (not (and x48 x135))) x22)) (not (and (not (and x118 (not (and (not (and x16 (not (and (not (and x85 x35)) (not (and x16 x96)))))) (not (and x38 x33)))))) (not (and x38 x135)))))) (x53 (> 0 (ite (> 4 x127) x127 (- x127 8))))) (let ((x70 (and x53 x126)) (x92 (not (and (not (and x53 x74)) (or (and (not (and x76 x97)) (not x53)) x28))))) (let ((x24 (not (and (not x70) (not (and x79 x92)))))) (let ((x77 (and (not x75) x120)) (x87 (and (not (and x24 x68)) (not (and x29 x92))))) (let ((x34 (not (and (or x105 (and (not (and (not x87) (not x77))) (not (and x87 x77)))) (not (and x92 x85))))) (x132 (not (and x24 x16)))) (let ((x139 (and x39 x23)) (x90 (not (and x132 (not (and x33 x34)))))) (let ((x27 (ite x30 (ite x32 (ite x44 (ite x56 x107 0) x107) x107) (ite x44 (ite x56 x15 0) x15))) (x94 (not (and (or (and (not (and x109 (not x20))) (not (and x20 (and (not (and x90 x118)) (not (and x34 x135)))))) x23) (not (and x139 x34)))))) (let ((x103 (+ x27 1))) (let ((x141 (ite x22 false x109)) (x11 (ite x22 x131 (+ x131 1))) (x41 (not x137)) (x99 (not (< x103 4)))) (let ((x111 (ite x43 x11 0))) (let ((x81 (ite x41 (ite x99 x111 x11) x111))) (let ((x128 (ite x114 false (< (ite (< x81 4) x81 (- x81 8)) 0)))) (= (- (ite (not (or (or x114 (and (or (not (or x124 (or x63 (not (or x10 x43))))) (or x122 x58)) x57)) (and (not (and x67 x94)) (not (and (not (and (not (and x124 x94)) (not (and (not (and (not (and (not (and (not (and x70 x85)) x132)) x139)) (not (and x63 x90)))) (and x63 x129))))) x57))))) 1 0) (ite (ite (not (< (+ (ite x41 (ite x99 (ite x43 (ite x12 x103 0) x103) x103) (ite x43 (ite x12 x27 0) x27)) 1) 4)) (ite (not x58) (ite x122 (ite x99 (ite x43 (ite x12 (not (or x73 x87)) x141) false) x141) x128) false) x128) 1 0)) (+ x116 (* 128 x40)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) :named smtcomp1))
+(assert (! (> 128 x116) :named smtcomp2))
+(assert (! (< 0 x116) :named smtcomp3))
+(check-sat)
+(get-unsat-core)
+(exit)

test/regression/unsatcores/QF_LIA/calypto-1.smt2.expected.err

@@ -0,0 +1,6 @@
+unsat
+(
+smtcomp1
+smtcomp2
+smtcomp3
+)

test/regression/unsatcores/QF_LIA/calypto-1.smt2.expected.out

@@ -0,0 +1,27 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+(set-logic QF_LIA)
+(declare-fun x83 () Bool)
+(declare-fun x60 () Bool)
+(declare-fun x113 () Bool)
+(declare-fun x58 () Bool)
+(declare-fun x51 () Bool)
+(declare-fun x65 () Bool)
+(declare-fun x46 () Bool)
+(declare-fun x5 () Bool)
+(declare-fun x59 () Bool)
+(declare-fun x138 () Bool)
+(declare-fun x95 () Bool)
+(declare-fun x54 () Bool)
+(declare-fun x62 () Bool)
+(declare-fun x112 () Bool)
+(declare-fun x9 () Bool)
+(declare-fun x116 () Int)
+(declare-fun x49 () Bool)
+(declare-fun x40 () Int)
+(assert (! (let ((x66 (ite (not x62) x138 false)) (x21 (not x54)) (x26 (not x59))) (let ((x19 (ite x26 (ite x21 x66 true) x66)) (x2 (not x113))) (let ((x64 (not (not x19))) (x50 (ite x2 true false)) (x89 (not x51))) (let ((x82 (ite x64 false (ite x89 x50 true))) (x13 (not x95))) (let ((x80 (ite x13 true false)) (x130 (not x82)) (x121 (not x46))) (let ((x125 (ite x66 1 0)) (x36 (not x66)) (x110 (ite x130 false (ite x121 x80 true)))) (let ((x7 (+ 1 x125))) (let ((x88 (ite x64 x7 (ite (ite x89 (ite x2 x66 false) x66) 1 0)))) (let ((x17 (+ x88 1))) (let ((x102 (ite x130 x17 (ite x121 (ite x13 x88 0) x88)))) (let ((x119 (not x110)) (x123 (+ 1 x102)) (x61 (not x36)) (x37 (not x83)) (x108 (not x5))) (let ((x15 (ite x119 (ite x61 (ite x108 (ite x37 x123 0) x123) x123) (ite x108 (ite x37 x102 0) x102)))) (let ((x107 (+ x15 1))) (let ((x124 (= 2 x107)) (x33 (= x123 2)) (x133 (ite x37 true false))) (let ((x104 (ite x108 x133 true))) (let ((x56 (not x9)) (x8 (ite x119 (ite x61 x104 false) x104))) (let ((x44 (not x60)) (x106 (ite x56 true false))) (let ((x72 (ite x44 x106 true)) (x30 (not x8)) (x32 (not (> 4 x107)))) (let ((x137 (ite x30 (ite x32 x72 false) x72))) (let ((x115 (or (ite x44 (ite x108 (ite x121 (ite x89 (ite x26 x66 false) false) false) false) false) x112)) (x10 (not (or x137 x33))) (x43 (not x65))) (let ((x39 (or (or x10 x115) x65))) (let ((x79 (= 2 x17)) (x122 (not (or (ite x43 (ite x44 (ite x108 (ite x121 (ite x89 (ite x26 x54 false) false) false) false) false) false) x49))) (x63 (not x39)) (x12 (not x115))) (let ((x45 (not (or x79 x8))) (x78 (and x119 x36))) (let ((x28 (and (not x78) (or x78 (not (ite x108 x83 false)))))) (let ((x100 (not x28))) (let ((x29 (and (not x79) x100))) (let ((x68 (not x29))) (let ((x105 (and (or (not (ite x44 x9 false)) x45) x68))) (let ((x134 (not x105))) (let ((x135 (and (not x33) x134))) (let ((x118 (not x135))) (let ((x129 (not x124)) (x23 (and (or (or x65 x12) x10) x118))) (let ((x67 (and x129 (not x23)))) (let ((x93 (ite x21 x125 x7)) (x57 (not x67)) (x114 (not x49))) (let ((x3 (ite x61 x93 (ite x26 x93 0)))) (let ((x42 (ite x2 x3 (+ x3 1)))) (let ((x117 (ite x64 x42 (ite x89 x42 0)))) (let ((x98 (ite x13 x117 (+ x117 1)))) (let ((x127 (ite x130 x98 (ite x121 x98 0)))) (let ((x47 (ite x37 x127 (+ 1 x127)))) (let ((x31 (ite x108 x47 0))) (let ((x1 (ite x119 (ite x61 x31 x47) x31))) (let ((x91 (ite x56 x1 (+ x1 1)))) (let ((x14 (ite x44 x91 0))) (let ((x131 (ite x30 (ite x32 x14 x91) x14))) (let ((x4 (not (ite x61 (ite x21 x66 false) x19))) (x109 (< (ite (< x131 4) x131 (- x131 8)) 0)) (x86 (not (or x50 x82)))) (let ((x71 (not (or (not (or x86 x4)) (and x86 x4))))) (let ((x25 (or (not (or x71 (not (and x80 x119)))) (and (not (or x80 x110)) x71)))) (let ((x84 (not x25)) (x74 (not (or x78 x108)))) (let ((x140 (or (or (not (or (not (and x133 x100)) x84)) (and x25 x74)) (and x84 (not (or x133 x28))))) (x126 (not (or x5 (or x78 x83))))) (let ((x101 (not (and (not (and x140 x79)) (not (and x126 (and x66 x25))))))) (let ((x136 (and (not (and x29 x140)) (not (and x101 x68))))) (let ((x97 (not (or x133 x84))) (x55 (not (or x71 x80))) (x6 (not (or (not (or x21 x36)) (not (or x50 x4))))) (x120 (not (or x106 x136)))) (let ((x76 (or (not (or x55 x6)) (and x55 x6)))) (let ((x18 (not x76))) (let ((x52 (not (and (or (not (or (and x18 x97) (not (or x18 x97)))) x28) (not (and x74 x76))))) (x35 (and (and x76 x66) x126))) (let ((x96 (not (and (not (and x35 x126)) (not (and x79 x52)))))) (let ((x69 (or x60 (or x45 x9))) (x75 (and (not (and x96 x68)) (not (and x29 x52))))) (let ((x85 (and x105 x69))) (let ((x73 (or x105 x106)) (x38 (not (and (not (and x52 x85)) (or (not (or (and x75 x120) (not (or x120 x75)))) x105)))) (x16 (not x69))) (let ((x22 (not x112)) (x48 (or (and x136 (not x73)) (or (not (or (not (and x106 x134)) x136)) (and x140 x85))))) (let ((x20 (and (not (or (and (not (and (not (and (not (and x33 x48)) (not (and x101 x16)))) x118)) (not (and x48 x135))) x22)) (not (and (not (and x118 (not (and (not (and x16 (not (and (not (and x85 x35)) (not (and x16 x96)))))) (not (and x38 x33)))))) (not (and x38 x135)))))) (x53 (> 0 (ite (> 4 x127) x127 (- x127 8))))) (let ((x70 (and x53 x126)) (x92 (not (and (not (and x53 x74)) (or (and (not (and x76 x97)) (not x53)) x28))))) (let ((x24 (not (and (not x70) (not (and x79 x92)))))) (let ((x77 (and (not x75) x120)) (x87 (and (not (and x24 x68)) (not (and x29 x92))))) (let ((x34 (not (and (or x105 (and (not (and (not x87) (not x77))) (not (and x87 x77)))) (not (and x92 x85))))) (x132 (not (and x24 x16)))) (let ((x139 (and x39 x23)) (x90 (not (and x132 (not (and x33 x34)))))) (let ((x27 (ite x30 (ite x32 (ite x44 (ite x56 x107 0) x107) x107) (ite x44 (ite x56 x15 0) x15))) (x94 (not (and (or (and (not (and x109 (not x20))) (not (and x20 (and (not (and x90 x118)) (not (and x34 x135)))))) x23) (not (and x139 x34)))))) (let ((x103 (+ x27 1))) (let ((x141 (ite x22 false x109)) (x11 (ite x22 x131 (+ x131 1))) (x41 (not x137)) (x99 (not (< x103 4)))) (let ((x111 (ite x43 x11 0))) (let ((x81 (ite x41 (ite x99 x111 x11) x111))) (let ((x128 (ite x114 false (< (ite (< x81 4) x81 (- x81 8)) 0)))) (= (- (ite (not (or (or x114 (and (or (not (or x124 (or x63 (not (or x10 x43))))) (or x122 x58)) x57)) (and (not (and x67 x94)) (not (and (not (and (not (and x124 x94)) (not (and (not (and (not (and (not (and (not (and x70 x85)) x132)) x139)) (not (and x63 x90)))) (and x63 x129))))) x57))))) 1 0) (ite (ite (not (< (+ (ite x41 (ite x99 (ite x43 (ite x12 x103 0) x103) x103) (ite x43 (ite x12 x27 0) x27)) 1) 4)) (ite (not x58) (ite x122 (ite x99 (ite x43 (ite x12 (not (or x73 x87)) x141) false) x141) x128) false) x128) 1 0)) (+ x116 (* 128 x40)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) :named smtcomp1))
+(assert (! (> 128 x116) :named smtcomp2))
+(assert (! (< 0 x116) :named smtcomp3))
+(check-sat)
+(get-unsat-core)
+(exit)

test/regression/unsatcores/QF_LIA/calypto-1_min.smt2

@@ -0,0 +1,6 @@
+unsat
+(
+smtcomp1
+smtcomp2
+smtcomp3
+)

test/regression/unsatcores/QF_LIA/calypto-1_min.smt2.expected.err

@@ -0,0 +1,6 @@
+(set-option :produce-unsat-cores true)
+(set-logic QF_UF)
+(declare-const A Bool)
+(assert (! (ite A (not A) A) :named n))
+(check-sat)
+(get-unsat-core)

test/regression/unsatcores/QF_LIA/calypto-1_min.smt2.expected.out

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

test/regression/unsatcores/generic/ite-1.smt2

@@ -0,0 +1,9 @@
+(set-option :produce-unsat-cores true)
+(set-logic QF_UF)
+(declare-const A Bool)
+(declare-const B Bool)
+(declare-const C Bool)
+(assert (! (= A B) :named n1))
+(assert (! (ite C (not (=> A B)) (not (=> B A))) :named n2))
+(check-sat)
+(get-unsat-core)