diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 9bad711021a87ba2f71587111506520fa0db6749..d4208a8dd8a08b3d3a802942535c3925276bbbaf 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -25,7 +25,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
   private val z3cfg = new Z3Config(
     "MODEL" -> true,
     "MBQI" -> false,
-    "SOFT_TIMEOUT" -> 100,
+    // "SOFT_TIMEOUT" -> 100,
     "TYPE_CHECK" -> true,
     "WELL_SORTED_CHECK" -> true
     )
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index 23406bf71f025755741bf8d73b98372b96578934..80cf41defa936fcba933fc3e2fed2d95110af9e6 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -31,7 +31,7 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3Solve
   private val z3cfg = new Z3Config(
     "MODEL" -> true,
     "MBQI" -> false,
-    "SOFT_TIMEOUT" -> 100,
+    //"SOFT_TIMEOUT" -> 100,
     "TYPE_CHECK" -> true,
     "WELL_SORTED_CHECK" -> true
     )