diff --git a/lib/z3.jar b/lib/z3.jar
index 72cb5abd5c2db0b2a61d6e7c0eb3af91e1c6a2ae..7276c41cf889262a2fb06c375b99bcda888d7ca2 100644
Binary files a/lib/z3.jar and b/lib/z3.jar differ
diff --git a/src/purescala/AbstractZ3Solver.scala b/src/purescala/AbstractZ3Solver.scala
index 37575e0a166fd5f5b3bf110b6650f4c6071c6e53..1012269de47bec3ef314f9650acbf0661e3994f0 100644
--- a/src/purescala/AbstractZ3Solver.scala
+++ b/src/purescala/AbstractZ3Solver.scala
@@ -45,7 +45,7 @@ trait AbstractZ3Solver {
     }
 
     def boundConstraint(boundVar: Z3AST) : Z3AST = {
-      lowerBound <= boundVar && boundVar <= upperBound
+      z3.mkAnd(z3.mkLE(lowerBound, boundVar), z3.mkLE(boundVar, upperBound))
     }
 
     // for all recursive type roots
@@ -70,7 +70,7 @@ trait AbstractZ3Solver {
             val term = adtConstructors(child)(boundVars : _*)
             val pattern = z3.mkPattern(term)
             //val constraint = (fields zip boundVars).filter((p: (VarDecl, Z3AST)) => isUnbounded(p._1)).map((p: (VarDecl, Z3AST)) => boundConstraint(p._2)).foldLeft(z3.mkTrue)((a, b) => a && b)
-            val constraint = (fields zip boundVars).filter((p: (VarDecl, Z3AST)) => isUnbounded(p._1)).map((p: (VarDecl, Z3AST)) => boundConstraint(adtFieldSelectors(p._1.id)(term))).foldLeft(z3.mkTrue)((a, b) => a && b)
+            val constraint = (fields zip boundVars).filter((p: (VarDecl, Z3AST)) => isUnbounded(p._1)).map((p: (VarDecl, Z3AST)) => boundConstraint(adtFieldSelectors(p._1.id)(term))).foldLeft(z3.mkTrue)((a, b) => z3.mkAnd(a, b))
             val axiom = z3.mkForAll(0, List(pattern), fields.zipWithIndex.map{case (f, i) => (z3.mkIntSymbol(i), typeToSort(f.getType))}, constraint)
             //println("Asserting: " + axiom)
             z3.assertCnstr(axiom)