diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 8ec0984ee1994371ad95a95b7367887c923d2ff5..2a981382e6f942120ec2afa2186c69c9bc8d6714 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -963,6 +963,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
           z3Vars = z3Vars - i
           rb
         }
+        case Waypoint(_, e) => rec(e)
         case e @ Error(_) => {
           val tpe = e.getType
           val newAST = z3.mkFreshConst("errorValue", typeToSort(tpe))