fix to static learning application in UF, resolves bug# 239

diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp
index ef00b58189404bbf71852e7cfdbb28cff189ed9b..cd9ee79c31dee861b506353d8adad341169e68ac 100644 (file)
--- a/src/theory/uf/morgan/theory_uf_morgan.cpp
+++ b/src/theory/uf/morgan/theory_uf_morgan.cpp
@@ -647,6 +647,7 @@ void TheoryUFMorgan::staticLearning(TNode n, NodeBuilder<>& learned) {
     // binary OR of binary ANDs of EQUALities
     if(n.getKind() == kind::OR && n.getNumChildren() == 2 &&
        n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 &&
+       n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 &&
        (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) &&
        (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) &&
        (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) &&

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 73901c328be495e2a0d242908e3d193d6de971fe..6ce2468b82d50339b30e31a9ac4151d94edf9bc5 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -84,7 +84,8 @@ BUG_TESTS = \
        bug168.smt \
        bug187.smt2 \
        bug216.smt2 \
-       bug220.smt2
+       bug220.smt2 \
+       bug239.smt
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 

diff --git a/test/regress/regress0/bug239.smt b/test/regress/regress0/bug239.smt
new file mode 100644 (file)
index 0000000..b80f56c
--- /dev/null
+++ b/test/regress/regress0/bug239.smt
@@ -0,0 +1,185 @@
+(benchmark fuzzsmt
+:logic QF_LRA
+:status sat
+:extrafuns ((v0 Real))
+:extrafuns ((v1 Real))
+:extrafuns ((v2 Real))
+:formula
+(let (?e3 5)
+(let (?e4 0)
+(let (?e5 2)
+(let (?e6 (+ v0 v1))
+(let (?e7 (* v1 ?e3))
+(let (?e8 (~ v0))
+(let (?e9 (- v2 v1))
+(let (?e10 (- v0 ?e9))
+(let (?e11 (* v0 (~ ?e3)))
+(let (?e12 (/ ?e4 (~ ?e3)))
+(let (?e13 (+ ?e8 ?e7))
+(let (?e14 (/ ?e4 (~ ?e5)))
+(flet ($e15 (<= v2 ?e7))
+(flet ($e16 (<= ?e11 ?e11))
+(flet ($e17 (= ?e11 ?e13))
+(flet ($e18 (<= ?e7 ?e14))
+(flet ($e19 (> ?e14 v1))
+(flet ($e20 (< v0 ?e10))
+(flet ($e21 (= ?e8 ?e11))
+(flet ($e22 (>= ?e8 ?e13))
+(flet ($e23 (< ?e10 v2))
+(flet ($e24 (>= ?e10 ?e8))
+(flet ($e25 (= ?e6 ?e7))
+(flet ($e26 (distinct ?e12 ?e11))
+(flet ($e27 (distinct ?e10 ?e9))
+(let (?e28 (ite $e27 ?e13 ?e6))
+(let (?e29 (ite $e21 v2 ?e28))
+(let (?e30 (ite $e26 ?e12 ?e12))
+(let (?e31 (ite $e18 ?e28 v0))
+(let (?e32 (ite $e20 ?e9 ?e10))
+(let (?e33 (ite $e22 ?e11 ?e28))
+(let (?e34 (ite $e17 ?e8 ?e13))
+(let (?e35 (ite $e26 ?e14 v1))
+(let (?e36 (ite $e21 ?e14 ?e30))
+(let (?e37 (ite $e19 ?e7 ?e11))
+(let (?e38 (ite $e25 v1 ?e8))
+(let (?e39 (ite $e22 ?e28 ?e28))
+(let (?e40 (ite $e25 v0 ?e14))
+(let (?e41 (ite $e24 ?e37 v2))
+(let (?e42 (ite $e16 ?e6 v2))
+(let (?e43 (ite $e19 ?e11 ?e7))
+(let (?e44 (ite $e23 ?e36 v2))
+(let (?e45 (ite $e20 v1 ?e7))
+(let (?e46 (ite $e15 ?e45 ?e13))
+(flet ($e47 (= ?e32 ?e9))
+(flet ($e48 (< ?e41 v0))
+(flet ($e49 (distinct ?e14 ?e43))
+(flet ($e50 (distinct ?e8 ?e10))
+(flet ($e51 (> ?e8 ?e37))
+(flet ($e52 (< v1 ?e11))
+(flet ($e53 (< ?e30 ?e8))
+(flet ($e54 (< v2 ?e12))
+(flet ($e55 (>= ?e8 ?e31))
+(flet ($e56 (= ?e12 ?e44))
+(flet ($e57 (= ?e45 v0))
+(flet ($e58 (= ?e36 ?e39))
+(flet ($e59 (= ?e31 v0))
+(flet ($e60 (< ?e9 ?e43))
+(flet ($e61 (distinct ?e14 ?e44))
+(flet ($e62 (= ?e45 ?e29))
+(flet ($e63 (<= ?e12 ?e9))
+(flet ($e64 (>= ?e41 ?e28))
+(flet ($e65 (<= ?e11 v0))
+(flet ($e66 (< ?e29 ?e14))
+(flet ($e67 (< ?e44 v2))
+(flet ($e68 (< ?e40 ?e45))
+(flet ($e69 (> ?e34 ?e7))
+(flet ($e70 (= ?e38 ?e30))
+(flet ($e71 (>= ?e36 ?e31))
+(flet ($e72 (= ?e32 ?e38))
+(flet ($e73 (<= ?e30 ?e42))
+(flet ($e74 (= ?e11 ?e9))
+(flet ($e75 (> ?e40 ?e7))
+(flet ($e76 (distinct ?e39 ?e41))
+(flet ($e77 (< ?e11 ?e28))
+(flet ($e78 (distinct ?e31 ?e45))
+(flet ($e79 (= ?e45 ?e11))
+(flet ($e80 (>= ?e11 ?e42))
+(flet ($e81 (< ?e12 ?e7))
+(flet ($e82 (>= ?e11 ?e41))
+(flet ($e83 (<= ?e8 v0))
+(flet ($e84 (< ?e8 ?e8))
+(flet ($e85 (> ?e30 v2))
+(flet ($e86 (= ?e9 ?e30))
+(flet ($e87 (= ?e33 ?e7))
+(flet ($e88 (<= ?e32 ?e44))
+(flet ($e89 (<= ?e36 ?e33))
+(flet ($e90 (distinct ?e45 ?e45))
+(flet ($e91 (distinct ?e14 ?e44))
+(flet ($e92 (<= v1 ?e12))
+(flet ($e93 (>= v0 ?e12))
+(flet ($e94 (>= ?e46 ?e29))
+(flet ($e95 (> ?e14 ?e6))
+(flet ($e96 (>= v2 ?e14))
+(flet ($e97 (>= ?e39 ?e44))
+(flet ($e98 (>= ?e38 ?e28))
+(flet ($e99 (> v2 ?e9))
+(flet ($e100 (<= ?e42 ?e33))
+(flet ($e101 (= ?e30 ?e29))
+(flet ($e102 (= ?e9 v0))
+(flet ($e103 (distinct ?e37 ?e40))
+(flet ($e104 (= ?e43 ?e14))
+(flet ($e105 (<= ?e35 ?e13))
+(flet ($e106 (and $e102 $e70))
+(flet ($e107 (implies $e84 $e84))
+(flet ($e108 (implies $e69 $e60))
+(flet ($e109 (iff $e105 $e99))
+(flet ($e110 (iff $e100 $e80))
+(flet ($e111 (or $e52 $e86))
+(flet ($e112 (xor $e26 $e18))
+(flet ($e113 (or $e20 $e107))
+(flet ($e114 (not $e94))
+(flet ($e115 (or $e79 $e104))
+(flet ($e116 (not $e76))
+(flet ($e117 (if_then_else $e112 $e22 $e90))
+(flet ($e118 (xor $e77 $e57))
+(flet ($e119 (xor $e88 $e55))
+(flet ($e120 (and $e92 $e68))
+(flet ($e121 (or $e82 $e25))
+(flet ($e122 (implies $e19 $e119))
+(flet ($e123 (implies $e66 $e117))
+(flet ($e124 (if_then_else $e15 $e73 $e65))
+(flet ($e125 (iff $e64 $e103))
+(flet ($e126 (iff $e121 $e122))
+(flet ($e127 (if_then_else $e50 $e47 $e101))
+(flet ($e128 (iff $e81 $e127))
+(flet ($e129 (implies $e124 $e21))
+(flet ($e130 (iff $e87 $e129))
+(flet ($e131 (iff $e116 $e51))
+(flet ($e132 (implies $e72 $e97))
+(flet ($e133 (and $e56 $e98))
+(flet ($e134 (implies $e91 $e53))
+(flet ($e135 (xor $e133 $e114))
+(flet ($e136 (xor $e17 $e110))
+(flet ($e137 (iff $e96 $e128))
+(flet ($e138 (or $e125 $e59))
+(flet ($e139 (or $e23 $e48))
+(flet ($e140 (iff $e62 $e95))
+(flet ($e141 (not $e61))
+(flet ($e142 (and $e132 $e63))
+(flet ($e143 (xor $e109 $e131))
+(flet ($e144 (iff $e54 $e126))
+(flet ($e145 (xor $e74 $e67))
+(flet ($e146 (if_then_else $e89 $e93 $e140))
+(flet ($e147 (iff $e71 $e138))
+(flet ($e148 (and $e143 $e146))
+(flet ($e149 (xor $e147 $e142))
+(flet ($e150 (implies $e85 $e58))
+(flet ($e151 (or $e24 $e78))
+(flet ($e152 (if_then_else $e137 $e113 $e123))
+(flet ($e153 (and $e145 $e16))
+(flet ($e154 (not $e150))
+(flet ($e155 (implies $e151 $e154))
+(flet ($e156 (if_then_else $e118 $e136 $e75))
+(flet ($e157 (and $e108 $e108))
+(flet ($e158 (or $e83 $e141))
+(flet ($e159 (iff $e155 $e149))
+(flet ($e160 (iff $e158 $e156))
+(flet ($e161 (or $e115 $e130))
+(flet ($e162 (or $e157 $e160))
+(flet ($e163 (if_then_else $e152 $e153 $e139))
+(flet ($e164 (not $e144))
+(flet ($e165 (not $e27))
+(flet ($e166 (or $e148 $e162))
+(flet ($e167 (iff $e134 $e166))
+(flet ($e168 (or $e111 $e159))
+(flet ($e169 (or $e106 $e164))
+(flet ($e170 (xor $e161 $e120))
+(flet ($e171 (and $e168 $e165))
+(flet ($e172 (or $e170 $e135))
+(flet ($e173 (or $e169 $e163))
+(flet ($e174 (implies $e49 $e172))
+(flet ($e175 (xor $e174 $e173))
+(flet ($e176 (and $e171 $e175))
+(flet ($e177 (implies $e167 $e176))
+$e177
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+