Evaluator case when postcondition of undefined funciton was violated

src/main/scala/leon/Evaluator.scala

@@ -24,11 +24,16 @@ object Evaluator {
   case class InfiniteComputation() extends EvaluationResult {
     val finalResult = None
   }
+  case class PostconditionViolationFunctionFromModel() extends EvaluationResult {
+    val finalResult = None
+  }
+  
 
   def eval(context: EvaluationContext, expression: Expr, evaluator: Option[(EvaluationContext)=>Boolean], maxSteps: Int=500000) : EvaluationResult = {
     case class RuntimeErrorEx(msg: String) extends Exception
     case class InfiniteComputationEx() extends Exception
     case class TypeErrorEx(typeError: TypeError) extends Exception
+    case class PostconditionViolationFunctionFromModelEx() extends Exception
 
     var left: Int = maxSteps
 
@@ -96,6 +101,7 @@ object Evaluator {
             val postBody = replace(Map(ResultVariable() -> Variable(freshResID)), matchToIfThenElse(fd.postcondition.get))
             rec(frame + ((freshResID -> callResult)), postBody) match {
               case BooleanLiteral(true) => ;
+              case BooleanLiteral(false) if !fd.hasImplementation => throw PostconditionViolationFunctionFromModelEx()
               case BooleanLiteral(false) => throw RuntimeErrorEx("Postcondition violation for " + fd.id.name + " reached in evaluation.")
               case other => throw TypeErrorEx(TypeError(other, BooleanType))
             }
@@ -307,6 +313,7 @@ object Evaluator {
           case RuntimeErrorEx(msg) => RuntimeError(msg)
           case InfiniteComputationEx() => InfiniteComputation()
           case TypeErrorEx(te) => te
+          case PostconditionViolationFunctionFromModelEx() => PostconditionViolationFunctionFromModel()
         }
     }
   }

src/main/scala/leon/FairZ3Solver.scala

@@ -827,6 +827,10 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
           reporter.info("- Invalid model.")
           (false, asMap)
         }
+        case PostconditionViolationFunctionFromModel() => {
+          reporter.info("- Invalid Model: postcondition violation of a function that whose implementation was specified by the model")
+          (false, asMap)
+        }
         case other => {
           reporter.error("Something went wrong. While evaluating the model, we got this: " + other)
           (false, asMap)