Fixes for two bugs:

* one that Tim found in model generation for records containing Booleans
* another that the fuzzer found in quantifiers + check-models

Test cases enabled/added for both.

diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index fb80b27f7b584ec9d3f87185f02f642f6008c8b4..de1a60da40eef39c6ae54f462fa80f0b77b78876 100644 (file)
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -48,6 +48,31 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
       return NodeManager::currentNM()->mkConst(tf);
     }
   }
+  if(n.getType().isBoolean()) {
+    bool tf = n.getConst<bool>();
+    if(asType.isBitVector(1u)) {
+      return NodeManager::currentNM()->mkConst(BitVector(1u, tf ? 1u : 0u));
+    }
+    if(asType.isDatatype() && asType.hasAttribute(BooleanTermAttr())) {
+      const Datatype& asDatatype = asType.getConst<Datatype>();
+      return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, (tf ? asDatatype[0] : asDatatype[1]).getConstructor());
+    }
+  }
+  if(n.getType().isRecord() && asType.isRecord()) {
+    Debug("boolean-terms") << "+++ got a record - rewriteAs " << n << " : " << asType << endl;
+    const Record& rec CVC4_UNUSED = n.getType().getConst<Record>();
+    const Record& asRec = asType.getConst<Record>();
+    Assert(rec.getNumFields() == asRec.getNumFields());
+    Assert(n.getNumChildren() == asRec.getNumFields());
+    NodeBuilder<> b(n.getKind());
+    b << asType;
+    for(size_t i = 0; i < n.getNumChildren(); ++i) {
+      b << rewriteAs(n[i], TypeNode::fromType(asRec[i].second));
+    }
+    Node out = b;
+    Debug("boolean-terms") << "+++ returning record " << out << endl;
+    return out;
+  }
   Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl;
   if(n.getType().isArray()) {
     Assert(asType.isArray());

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 2c5844cd4a4e321aa890c961bb0be48844007f74..b4ac8d27e7d15f5a9d13480ae4c2a28a2489ce9e 100644 (file)
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -51,7 +51,9 @@ Node TheoryModel::getValue( TNode n ) const{
   //apply substitutions
   Node nn = d_substitutions.apply( n );
   //get value in model
-  return getModelValue( nn );
+  nn = getModelValue( nn );
+  Assert(nn.isConst() || nn.getKind() == kind::LAMBDA);
+  return nn;
 }
 
 Expr TheoryModel::getValue( Expr expr ) const{
@@ -150,7 +152,6 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
       if(val.getKind() == kind::CARDINALITY_CONSTRAINT) {
         val = NodeManager::currentNM()->mkConst(getCardinality(val[0].getType().toType()).getFiniteCardinality() <= val[1].getConst<Rational>().getNumerator());
       }
-      Assert(hasBoundVars || val.isConst());
       return val;
     }
 

diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index d58798b9826276a18be8bf97e2cccd334b115061..a649cfef546943dbd4e70fccb51d76eaa8ad8903 100644 (file)
--- a/test/regress/regress0/auflia/Makefile.am
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -21,6 +21,7 @@ TESTS =       \
        fuzz04.smt \
        fuzz05.smt \
        fuzz06.smt \
+       fuzz-error232.smt \
        a17.smt \
        error72.delta2.smt \
        x2.smt

diff --git a/test/regress/regress0/auflia/fuzz-error232.smt b/test/regress/regress0/auflia/fuzz-error232.smt
new file mode 100644 (file)
index 0000000..e8319c7
--- /dev/null
+++ b/test/regress/regress0/auflia/fuzz-error232.smt
@@ -0,0 +1,508 @@
+(benchmark fuzzsmt
+:logic AUFLIA
+:status sat
+:extrafuns ((f0 Int Int))
+:extrafuns ((f1 Array Array Array Array))
+:extrapreds ((p0 Int))
+:extrapreds ((p1 Array Array))
+:extrafuns ((v0 Int))
+:extrafuns ((v1 Int))
+:extrafuns ((v2 Int))
+:extrafuns ((v3 Array))
+:assumption
+(exists (?qvar0 Int) (?qvar1 Int) 
+(flet ($qf0 (p0 ?qvar1))
+(flet ($qf1 (p0 ?qvar0))
+(flet ($qf2 (or $qf0 $qf0))
+(flet ($qf3 (or $qf1 $qf2))
+$qf3
+)))))
+:formula
+(let (?e4 14)
+(let (?e5 3)
+(let (?e6 (- v1 v1))
+(let (?e7 (- v2 v2))
+(let (?e8 (~ v0))
+(let (?e9 (ite (p0 v0) 1 0))
+(let (?e10 (* v2 (~ ?e4)))
+(let (?e11 (* ?e4 ?e6))
+(let (?e12 (- ?e7 ?e8))
+(let (?e13 (* ?e4 ?e10))
+(let (?e14 (* v0 ?e5))
+(let (?e15 (~ ?e10))
+(let (?e16 (- ?e15 ?e14))
+(let (?e17 (+ ?e12 v1))
+(let (?e18 (ite (p0 ?e17) 1 0))
+(let (?e19 (~ ?e16))
+(let (?e20 (f0 ?e14))
+(let (?e21 (store v3 ?e7 v2))
+(let (?e22 (select v3 ?e11))
+(let (?e23 (f1 ?e21 v3 ?e21))
+(flet ($e24 (p1 ?e21 ?e23))
+(flet ($e25 (p1 ?e23 v3))
+(flet ($e26 (>= ?e22 ?e8))
+(flet ($e27 (<= ?e20 ?e20))
+(flet ($e28 (p0 ?e7))
+(flet ($e29 (< ?e19 ?e8))
+(flet ($e30 (>= ?e6 ?e14))
+(flet ($e31 (< ?e12 v2))
+(flet ($e32 (= ?e16 ?e18))
+(flet ($e33 (< ?e10 ?e10))
+(flet ($e34 (> ?e19 v2))
+(flet ($e35 (distinct ?e17 v0))
+(flet ($e36 (< v1 ?e15))
+(flet ($e37 (>= ?e15 v2))
+(flet ($e38 (<= ?e9 ?e19))
+(flet ($e39 (<= ?e13 ?e6))
+(flet ($e40 (p0 ?e11))
+(let (?e41 (ite $e39 ?e21 v3))
+(let (?e42 (ite $e36 ?e23 ?e23))
+(let (?e43 (ite $e34 v3 ?e21))
+(let (?e44 (ite $e29 ?e43 ?e21))
+(let (?e45 (ite $e24 ?e41 ?e44))
+(let (?e46 (ite $e35 ?e45 ?e42))
+(let (?e47 (ite $e37 ?e45 ?e23))
+(let (?e48 (ite $e28 ?e46 ?e41))
+(let (?e49 (ite $e25 ?e42 ?e44))
+(let (?e50 (ite $e35 ?e41 v3))
+(let (?e51 (ite $e29 ?e43 ?e50))
+(let (?e52 (ite $e27 ?e49 ?e43))
+(let (?e53 (ite $e40 ?e46 ?e23))
+(let (?e54 (ite $e33 ?e23 ?e46))
+(let (?e55 (ite $e40 ?e42 v3))
+(let (?e56 (ite $e28 ?e49 ?e51))
+(let (?e57 (ite $e26 ?e46 ?e21))
+(let (?e58 (ite $e32 ?e44 ?e52))
+(let (?e59 (ite $e30 ?e55 ?e54))
+(let (?e60 (ite $e25 ?e46 ?e54))
+(let (?e61 (ite $e31 ?e58 ?e59))
+(let (?e62 (ite $e38 ?e50 ?e48))
+(let (?e63 (ite $e37 ?e18 ?e15))
+(let (?e64 (ite $e39 ?e13 ?e15))
+(let (?e65 (ite $e36 v0 ?e13))
+(let (?e66 (ite $e31 ?e8 ?e10))
+(let (?e67 (ite $e28 ?e9 ?e12))
+(let (?e68 (ite $e25 v0 ?e18))
+(let (?e69 (ite $e33 ?e14 ?e22))
+(let (?e70 (ite $e30 ?e16 ?e64))
+(let (?e71 (ite $e33 v2 ?e66))
+(let (?e72 (ite $e34 ?e6 ?e13))
+(let (?e73 (ite $e26 ?e7 v2))
+(let (?e74 (ite $e37 ?e17 ?e65))
+(let (?e75 (ite $e26 ?e11 ?e64))
+(let (?e76 (ite $e33 ?e19 ?e68))
+(let (?e77 (ite $e27 ?e67 ?e73))
+(let (?e78 (ite $e34 ?e10 ?e16))
+(let (?e79 (ite $e40 ?e15 ?e6))
+(let (?e80 (ite $e37 ?e71 ?e70))
+(let (?e81 (ite $e31 v1 ?e73))
+(let (?e82 (ite $e32 ?e75 ?e64))
+(let (?e83 (ite $e35 ?e7 ?e67))
+(let (?e84 (ite $e38 ?e78 ?e66))
+(let (?e85 (ite $e24 ?e7 ?e11))
+(let (?e86 (ite $e29 ?e10 v0))
+(let (?e87 (ite $e32 ?e20 ?e80))
+(let (?e88 (store ?e23 ?e85 ?e17))
+(let (?e89 (select ?e53 ?e87))
+(let (?e90 (store ?e54 ?e20 ?e17))
+(let (?e91 (f1 ?e56 ?e59 ?e54))
+(let (?e92 (f1 v3 ?e54 ?e58))
+(let (?e93 (f1 ?e52 ?e52 v3))
+(let (?e94 (f1 ?e61 ?e50 ?e21))
+(let (?e95 (f1 ?e61 ?e43 ?e58))
+(let (?e96 (f1 ?e53 ?e53 ?e53))
+(let (?e97 (f1 ?e51 ?e54 ?e49))
+(let (?e98 (f1 ?e55 ?e55 ?e92))
+(let (?e99 (f1 ?e45 ?e55 ?e62))
+(let (?e100 (f1 ?e49 ?e50 ?e53))
+(let (?e101 (f1 ?e49 ?e52 ?e60))
+(let (?e102 (f1 ?e59 ?e97 ?e44))
+(let (?e103 (f1 ?e23 ?e47 ?e50))
+(let (?e104 (f1 ?e88 ?e98 ?e59))
+(let (?e105 (f1 ?e42 ?e42 ?e42))
+(let (?e106 (f1 ?e48 ?e47 ?e92))
+(let (?e107 (f1 ?e46 ?e46 ?e92))
+(let (?e108 (f1 ?e62 ?e104 ?e55))
+(let (?e109 (f1 ?e45 ?e59 ?e93))
+(let (?e110 (f1 ?e41 ?e41 ?e41))
+(let (?e111 (f1 ?e49 ?e57 ?e42))
+(let (?e112 (f1 ?e53 ?e91 ?e106))
+(let (?e113 (f1 ?e90 ?e90 ?e59))
+(let (?e114 (+ ?e18 ?e73))
+(let (?e115 (- ?e71 ?e17))
+(let (?e116 (~ ?e75))
+(let (?e117 (~ ?e115))
+(let (?e118 (+ ?e10 ?e18))
+(let (?e119 (ite (p0 ?e115) 1 0))
+(let (?e120 (* (~ ?e4) ?e6))
+(let (?e121 (* ?e63 (~ ?e4)))
+(let (?e122 (~ ?e6))
+(let (?e123 (* ?e19 ?e5))
+(let (?e124 (~ ?e16))
+(let (?e125 (- ?e65 ?e117))
+(let (?e126 (* ?e5 ?e80))
+(let (?e127 (~ ?e83))
+(let (?e128 (ite (p0 ?e86) 1 0))
+(let (?e129 (* (~ ?e5) ?e118))
+(let (?e130 (ite (p0 ?e85) 1 0))
+(let (?e131 (* ?e4 ?e118))
+(let (?e132 (f0 ?e69))
+(let (?e133 (- ?e20 ?e15))
+(let (?e134 (* ?e64 ?e5))
+(let (?e135 (f0 ?e9))
+(let (?e136 (f0 ?e74))
+(let (?e137 (~ ?e22))
+(let (?e138 (* ?e77 ?e5))
+(let (?e139 (ite (p0 ?e81) 1 0))
+(let (?e140 (* (~ ?e5) ?e73))
+(let (?e141 (ite (p0 ?e65) 1 0))
+(let (?e142 (* ?e82 (~ ?e5)))
+(let (?e143 (ite (p0 ?e67) 1 0))
+(let (?e144 (- ?e120 ?e13))
+(let (?e145 (* ?e19 ?e5))
+(let (?e146 (f0 ?e87))
+(let (?e147 (f0 ?e76))
+(let (?e148 (ite (p0 ?e139) 1 0))
+(let (?e149 (ite (p0 ?e75) 1 0))
+(let (?e150 (ite (p0 ?e135) 1 0))
+(let (?e151 (~ ?e16))
+(let (?e152 (ite (p0 ?e66) 1 0))
+(let (?e153 (ite (p0 ?e11) 1 0))
+(let (?e154 (~ v0))
+(let (?e155 (* ?e5 ?e70))
+(let (?e156 (~ v2))
+(let (?e157 (~ ?e80))
+(let (?e158 (f0 ?e12))
+(let (?e159 (* ?e5 ?e72))
+(let (?e160 (f0 ?e64))
+(let (?e161 (~ ?e89))
+(let (?e162 (- ?e14 ?e79))
+(let (?e163 (f0 ?e14))
+(let (?e164 (+ ?e18 ?e69))
+(let (?e165 (* ?e68 (~ ?e5)))
+(let (?e166 (- ?e22 ?e124))
+(let (?e167 (ite (p0 ?e78) 1 0))
+(let (?e168 (* v1 (~ ?e5)))
+(let (?e169 (* (~ ?e4) ?e66))
+(let (?e170 (ite (p0 ?e136) 1 0))
+(let (?e171 (~ ?e80))
+(let (?e172 (ite (p0 ?e7) 1 0))
+(let (?e173 (f0 ?e139))
+(let (?e174 (- ?e20 ?e15))
+(let (?e175 (* ?e8 ?e4))
+(let (?e176 (+ ?e84 ?e76))
+(flet ($e177 (p1 ?e111 ?e105))
+(flet ($e178 (p1 ?e44 ?e54))
+(flet ($e179 (p1 ?e103 ?e88))
+(flet ($e180 (p1 ?e55 ?e104))
+(flet ($e181 (p1 ?e60 ?e43))
+(flet ($e182 (p1 ?e50 ?e111))
+(flet ($e183 (p1 ?e61 ?e101))
+(flet ($e184 (p1 ?e21 ?e107))
+(flet ($e185 (p1 ?e102 ?e88))
+(flet ($e186 (p1 ?e95 ?e98))
+(flet ($e187 (p1 ?e100 ?e47))
+(flet ($e188 (p1 ?e109 ?e92))
+(flet ($e189 (p1 ?e59 ?e62))
+(flet ($e190 (p1 ?e49 ?e102))
+(flet ($e191 (p1 ?e52 ?e103))
+(flet ($e192 (p1 ?e99 ?e93))
+(flet ($e193 (p1 v3 ?e96))
+(flet ($e194 (p1 ?e53 ?e21))
+(flet ($e195 (p1 ?e91 ?e112))
+(flet ($e196 (p1 ?e110 ?e90))
+(flet ($e197 (p1 ?e106 ?e93))
+(flet ($e198 (p1 ?e45 ?e94))
+(flet ($e199 (p1 ?e43 ?e107))
+(flet ($e200 (p1 ?e93 ?e57))
+(flet ($e201 (p1 ?e56 ?e45))
+(flet ($e202 (p1 ?e108 ?e88))
+(flet ($e203 (p1 ?e23 ?e54))
+(flet ($e204 (p1 ?e101 ?e21))
+(flet ($e205 (p1 ?e57 ?e58))
+(flet ($e206 (p1 ?e42 ?e44))
+(flet ($e207 (p1 ?e100 ?e48))
+(flet ($e208 (p1 ?e52 ?e57))
+(flet ($e209 (p1 ?e113 ?e93))
+(flet ($e210 (p1 ?e41 ?e92))
+(flet ($e211 (p1 ?e42 v3))
+(flet ($e212 (p1 ?e41 v3))
+(flet ($e213 (p1 ?e93 ?e57))
+(flet ($e214 (p1 ?e97 ?e46))
+(flet ($e215 (p1 ?e91 ?e97))
+(flet ($e216 (p1 ?e51 ?e44))
+(flet ($e217 (>= ?e132 ?e86))
+(flet ($e218 (distinct v2 ?e132))
+(flet ($e219 (<= ?e146 ?e164))
+(flet ($e220 (= ?e151 ?e164))
+(flet ($e221 (p0 ?e69))
+(flet ($e222 (p0 ?e157))
+(flet ($e223 (distinct ?e12 ?e116))
+(flet ($e224 (>= ?e8 ?e155))
+(flet ($e225 (> ?e66 ?e15))
+(flet ($e226 (<= ?e140 ?e13))
+(flet ($e227 (distinct ?e170 ?e115))
+(flet ($e228 (<= ?e162 ?e142))
+(flet ($e229 (>= ?e19 ?e163))
+(flet ($e230 (distinct ?e129 ?e70))
+(flet ($e231 (> ?e157 ?e175))
+(flet ($e232 (> ?e73 ?e13))
+(flet ($e233 (>= ?e81 ?e76))
+(flet ($e234 (>= ?e144 ?e135))
+(flet ($e235 (distinct ?e89 ?e170))
+(flet ($e236 (distinct ?e134 ?e161))
+(flet ($e237 (> ?e153 ?e8))
+(flet ($e238 (>= ?e124 ?e124))
+(flet ($e239 (= ?e162 ?e19))
+(flet ($e240 (<= ?e167 ?e166))
+(flet ($e241 (= ?e87 ?e137))
+(flet ($e242 (= ?e83 ?e159))
+(flet ($e243 (>= ?e174 ?e140))
+(flet ($e244 (distinct ?e77 ?e172))
+(flet ($e245 (p0 ?e122))
+(flet ($e246 (< ?e74 ?e12))
+(flet ($e247 (p0 ?e129))
+(flet ($e248 (> ?e123 ?e127))
+(flet ($e249 (<= ?e114 ?e162))
+(flet ($e250 (<= ?e75 ?e11))
+(flet ($e251 (> ?e154 ?e147))
+(flet ($e252 (<= ?e125 ?e156))
+(flet ($e253 (>= ?e153 ?e89))
+(flet ($e254 (distinct ?e69 ?e154))
+(flet ($e255 (= ?e136 ?e87))
+(flet ($e256 (p0 ?e148))
+(flet ($e257 (> ?e131 ?e171))
+(flet ($e258 (<= ?e7 ?e86))
+(flet ($e259 (= ?e164 ?e172))
+(flet ($e260 (<= ?e126 v2))
+(flet ($e261 (>= ?e169 ?e172))
+(flet ($e262 (<= ?e67 ?e159))
+(flet ($e263 (p0 ?e79))
+(flet ($e264 (>= ?e143 ?e175))
+(flet ($e265 (<= ?e176 ?e165))
+(flet ($e266 (>= ?e10 ?e168))
+(flet ($e267 (= ?e80 ?e122))
+(flet ($e268 (<= ?e78 ?e82))
+(flet ($e269 (> ?e10 ?e122))
+(flet ($e270 (< v2 ?e165))
+(flet ($e271 (= ?e85 ?e138))
+(flet ($e272 (< ?e130 ?e170))
+(flet ($e273 (> ?e173 ?e18))
+(flet ($e274 (distinct ?e20 ?e71))
+(flet ($e275 (p0 ?e86))
+(flet ($e276 (p0 ?e14))
+(flet ($e277 (< ?e72 ?e114))
+(flet ($e278 (> ?e22 ?e75))
+(flet ($e279 (p0 ?e150))
+(flet ($e280 (p0 ?e139))
+(flet ($e281 (> ?e174 ?e151))
+(flet ($e282 (< ?e119 ?e22))
+(flet ($e283 (< ?e133 ?e14))
+(flet ($e284 (<= ?e9 v2))
+(flet ($e285 (distinct v0 ?e170))
+(flet ($e286 (<= ?e121 ?e136))
+(flet ($e287 (= ?e176 ?e85))
+(flet ($e288 (< ?e118 ?e123))
+(flet ($e289 (< ?e174 ?e63))
+(flet ($e290 (< ?e174 ?e19))
+(flet ($e291 (p0 ?e78))
+(flet ($e292 (distinct ?e160 ?e167))
+(flet ($e293 (<= ?e17 ?e18))
+(flet ($e294 (<= ?e147 ?e173))
+(flet ($e295 (distinct ?e68 ?e146))
+(flet ($e296 (< ?e117 ?e149))
+(flet ($e297 (>= ?e120 ?e168))
+(flet ($e298 (< ?e122 ?e74))
+(flet ($e299 (<= ?e66 ?e140))
+(flet ($e300 (= ?e141 ?e63))
+(flet ($e301 (p0 ?e132))
+(flet ($e302 (distinct ?e6 ?e14))
+(flet ($e303 (= ?e152 ?e133))
+(flet ($e304 (distinct ?e142 ?e153))
+(flet ($e305 (<= ?e145 ?e122))
+(flet ($e306 (>= ?e167 ?e123))
+(flet ($e307 (>= ?e128 ?e139))
+(flet ($e308 (> ?e12 ?e75))
+(flet ($e309 (distinct ?e84 ?e175))
+(flet ($e310 (> ?e64 ?e143))
+(flet ($e311 (p0 ?e158))
+(flet ($e312 (p0 ?e157))
+(flet ($e313 (<= v1 ?e18))
+(flet ($e314 (= ?e149 ?e119))
+(flet ($e315 (= ?e87 ?e127))
+(flet ($e316 (p0 ?e152))
+(flet ($e317 (p0 ?e16))
+(flet ($e318 (= ?e170 ?e124))
+(flet ($e319 (<= ?e157 ?e139))
+(flet ($e320 (>= ?e155 ?e66))
+(flet ($e321 (< ?e65 ?e118))
+(flet ($e322 (xor $e271 $e229))
+(flet ($e323 (iff $e237 $e269))
+(flet ($e324 (xor $e181 $e262))
+(flet ($e325 (and $e292 $e312))
+(flet ($e326 (not $e261))
+(flet ($e327 (xor $e193 $e310))
+(flet ($e328 (implies $e236 $e191))
+(flet ($e329 (and $e242 $e27))
+(flet ($e330 (xor $e295 $e326))
+(flet ($e331 (iff $e209 $e184))
+(flet ($e332 (not $e225))
+(flet ($e333 (if_then_else $e245 $e201 $e208))
+(flet ($e334 (iff $e251 $e234))
+(flet ($e335 (not $e239))
+(flet ($e336 (xor $e36 $e230))
+(flet ($e337 (implies $e314 $e333))
+(flet ($e338 (not $e316))
+(flet ($e339 (and $e222 $e223))
+(flet ($e340 (xor $e231 $e315))
+(flet ($e341 (and $e340 $e195))
+(flet ($e342 (xor $e220 $e29))
+(flet ($e343 (implies $e249 $e241))
+(flet ($e344 (implies $e332 $e182))
+(flet ($e345 (not $e330))
+(flet ($e346 (if_then_else $e30 $e246 $e185))
+(flet ($e347 (not $e337))
+(flet ($e348 (not $e240))
+(flet ($e349 (if_then_else $e183 $e328 $e278))
+(flet ($e350 (xor $e319 $e280))
+(flet ($e351 (and $e180 $e343))
+(flet ($e352 (or $e254 $e28))
+(flet ($e353 (and $e34 $e297))
+(flet ($e354 (if_then_else $e202 $e347 $e286))
+(flet ($e355 (iff $e320 $e226))
+(flet ($e356 (and $e227 $e268))
+(flet ($e357 (implies $e317 $e345))
+(flet ($e358 (or $e313 $e279))
+(flet ($e359 (and $e186 $e284))
+(flet ($e360 (iff $e256 $e33))
+(flet ($e361 (or $e346 $e196))
+(flet ($e362 (if_then_else $e39 $e302 $e289))
+(flet ($e363 (implies $e294 $e275))
+(flet ($e364 (iff $e192 $e276))
+(flet ($e365 (or $e204 $e358))
+(flet ($e366 (and $e235 $e212))
+(flet ($e367 (if_then_else $e197 $e194 $e348))
+(flet ($e368 (or $e362 $e199))
+(flet ($e369 (and $e270 $e215))
+(flet ($e370 (implies $e260 $e187))
+(flet ($e371 (not $e263))
+(flet ($e372 (not $e272))
+(flet ($e373 (not $e266))
+(flet ($e374 (and $e353 $e336))
+(flet ($e375 (implies $e368 $e283))
+(flet ($e376 (iff $e232 $e211))
+(flet ($e377 (if_then_else $e25 $e352 $e253))
+(flet ($e378 (implies $e377 $e200))
+(flet ($e379 (if_then_else $e219 $e264 $e288))
+(flet ($e380 (implies $e210 $e339))
+(flet ($e381 (iff $e35 $e217))
+(flet ($e382 (if_then_else $e306 $e309 $e351))
+(flet ($e383 (not $e304))
+(flet ($e384 (implies $e228 $e189))
+(flet ($e385 (or $e214 $e267))
+(flet ($e386 (and $e243 $e354))
+(flet ($e387 (xor $e341 $e350))
+(flet ($e388 (or $e281 $e366))
+(flet ($e389 (and $e324 $e274))
+(flet ($e390 (and $e322 $e375))
+(flet ($e391 (if_then_else $e387 $e305 $e359))
+(flet ($e392 (iff $e287 $e293))
+(flet ($e393 (or $e389 $e371))
+(flet ($e394 (or $e188 $e224))
+(flet ($e395 (iff $e216 $e325))
+(flet ($e396 (if_then_else $e300 $e258 $e364))
+(flet ($e397 (if_then_else $e395 $e394 $e32))
+(flet ($e398 (iff $e344 $e296))
+(flet ($e399 (and $e255 $e363))
+(flet ($e400 (not $e248))
+(flet ($e401 (or $e323 $e365))
+(flet ($e402 (not $e391))
+(flet ($e403 (not $e31))
+(flet ($e404 (not $e190))
+(flet ($e405 (and $e327 $e393))
+(flet ($e406 (or $e397 $e388))
+(flet ($e407 (xor $e329 $e342))
+(flet ($e408 (or $e298 $e299))
+(flet ($e409 (xor $e233 $e233))
+(flet ($e410 (not $e282))
+(flet ($e411 (implies $e40 $e356))
+(flet ($e412 (xor $e335 $e357))
+(flet ($e413 (implies $e402 $e376))
+(flet ($e414 (implies $e378 $e303))
+(flet ($e415 (and $e247 $e401))
+(flet ($e416 (and $e321 $e385))
+(flet ($e417 (not $e290))
+(flet ($e418 (not $e398))
+(flet ($e419 (iff $e360 $e38))
+(flet ($e420 (implies $e418 $e273))
+(flet ($e421 (implies $e415 $e411))
+(flet ($e422 (xor $e338 $e409))
+(flet ($e423 (not $e26))
+(flet ($e424 (xor $e413 $e218))
+(flet ($e425 (not $e285))
+(flet ($e426 (if_then_else $e422 $e396 $e252))
+(flet ($e427 (and $e291 $e412))
+(flet ($e428 (implies $e369 $e417))
+(flet ($e429 (or $e361 $e198))
+(flet ($e430 (implies $e406 $e24))
+(flet ($e431 (iff $e179 $e203))
+(flet ($e432 (implies $e238 $e428))
+(flet ($e433 (if_then_else $e355 $e349 $e318))
+(flet ($e434 (not $e177))
+(flet ($e435 (iff $e434 $e404))
+(flet ($e436 (xor $e207 $e384))
+(flet ($e437 (if_then_else $e37 $e380 $e250))
+(flet ($e438 (if_then_else $e259 $e433 $e370))
+(flet ($e439 (not $e400))
+(flet ($e440 (xor $e429 $e213))
+(flet ($e441 (implies $e308 $e257))
+(flet ($e442 (or $e403 $e440))
+(flet ($e443 (if_then_else $e432 $e221 $e178))
+(flet ($e444 (iff $e334 $e244))
+(flet ($e445 (iff $e383 $e386))
+(flet ($e446 (iff $e444 $e437))
+(flet ($e447 (or $e405 $e416))
+(flet ($e448 (if_then_else $e441 $e420 $e382))
+(flet ($e449 (iff $e419 $e390))
+(flet ($e450 (iff $e448 $e206))
+(flet ($e451 (xor $e265 $e424))
+(flet ($e452 (implies $e446 $e205))
+(flet ($e453 (implies $e438 $e450))
+(flet ($e454 (or $e447 $e453))
+(flet ($e455 (implies $e454 $e445))
+(flet ($e456 (xor $e451 $e410))
+(flet ($e457 (if_then_else $e455 $e442 $e439))
+(flet ($e458 (implies $e452 $e311))
+(flet ($e459 (implies $e423 $e407))
+(flet ($e460 (xor $e443 $e373))
+(flet ($e461 (iff $e457 $e331))
+(flet ($e462 (not $e459))
+(flet ($e463 (xor $e379 $e430))
+(flet ($e464 (xor $e461 $e301))
+(flet ($e465 (iff $e427 $e456))
+(flet ($e466 (if_then_else $e307 $e464 $e436))
+(flet ($e467 (not $e466))
+(flet ($e468 (iff $e462 $e426))
+(flet ($e469 (iff $e449 $e374))
+(flet ($e470 (or $e367 $e367))
+(flet ($e471 (implies $e408 $e470))
+(flet ($e472 (xor $e467 $e421))
+(flet ($e473 (or $e399 $e435))
+(flet ($e474 (or $e468 $e472))
+(flet ($e475 (or $e277 $e460))
+(flet ($e476 (iff $e471 $e381))
+(flet ($e477 (not $e476))
+(flet ($e478 (or $e392 $e431))
+(flet ($e479 (iff $e425 $e463))
+(flet ($e480 (or $e479 $e475))
+(flet ($e481 (if_then_else $e478 $e372 $e465))
+(flet ($e482 (if_then_else $e474 $e414 $e477))
+(flet ($e483 (xor $e482 $e480))
+(flet ($e484 (xor $e473 $e458))
+(flet ($e485 (xor $e484 $e483))
+(flet ($e486 (iff $e469 $e469))
+(flet ($e487 (if_then_else $e485 $e485 $e486))
+(flet ($e488 (iff $e487 $e481))
+$e488
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 2db03ff1cd2470e92c0aa4764fba26c48962c4be..06227ad3aaa97810fa990421d0df8deee0f651b3 100644 (file)
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -38,6 +38,7 @@ TESTS =       \
        typed_v2l30079.cvc \
        typed_v3l20092.cvc \
        typed_v5l30069.cvc \
+       boolean-equality.cvc \
        boolean-terms-datatype.cvc \
        boolean-terms-parametric-datatype-1.cvc \
        boolean-terms-parametric-datatype-2.cvc \