diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index 440d18efdc7002f4b89dc0e54ba815f51fc646ba..9c0292deb8fbd5e36bc9c40d4b42e3ca7b250ef9 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -234,7 +234,7 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
   }
 
   private var abstractedFormula = false
-  override def isSat(vc: Expr) = decide(vc, false)
+  override def isUnsat(vc: Expr) = decide(vc, false)
   def solve(vc: Expr) = decide(vc, true)
   def decide(vc: Expr, forValidity: Boolean) : Option[Boolean] = {
     abstractedFormula = false