Better return results when it is impossible to compute the model

src/main/scala/leon/Evaluator.scala

@@ -24,7 +24,7 @@ object Evaluator {
   case class InfiniteComputation() extends EvaluationResult {
     val finalResult = None
   }
-  case class PostconditionViolationFunctionFromModel() extends EvaluationResult {
+  case class ImpossibleComputation() extends EvaluationResult {
     val finalResult = None
   }
   
@@ -33,7 +33,7 @@ object Evaluator {
     case class RuntimeErrorEx(msg: String) extends Exception
     case class InfiniteComputationEx() extends Exception
     case class TypeErrorEx(typeError: TypeError) extends Exception
-    case class PostconditionViolationFunctionFromModelEx() extends Exception
+    case class ImpossibleComputationEx() extends Exception
 
     var left: Int = maxSteps
 
@@ -101,7 +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) if !fd.hasImplementation => throw ImpossibleComputationEx()
               case BooleanLiteral(false) => throw RuntimeErrorEx("Postcondition violation for " + fd.id.name + " reached in evaluation.")
               case other => throw TypeErrorEx(TypeError(other, BooleanType))
             }
@@ -313,7 +313,7 @@ object Evaluator {
           case RuntimeErrorEx(msg) => RuntimeError(msg)
           case InfiniteComputationEx() => InfiniteComputation()
           case TypeErrorEx(te) => te
-          case PostconditionViolationFunctionFromModelEx() => PostconditionViolationFunctionFromModel()
+          case ImpossibleComputationEx() => ImpossibleComputation()
         }
     }
   }

src/main/scala/leon/FairZ3Solver.scala

@@ -827,8 +827,8 @@ 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")
+        case ImpossibleComputation() => {
+          reporter.info("- Invalid Model: the model could not be verified because of insufficient information.")
           (false, asMap)
         }
         case other => {