3 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
index 296a2f475..8dddf5065 100644
--- a/src/theory/fp/theory_fp_type_rules.h
+++ b/src/theory/fp/theory_fp_type_rules.h
@@ -180,7 +180,7 @@ class FloatingPointRoundingOperationTypeRule {
       for (size_t i = 2; i < children; ++i) {
         if (!(n[i].getType(check) == firstOperand)) {
           throw TypeCheckingExceptionPrivate(
-              n, "floating-point test applied to mixed sorts");
+              n, "floating-point operation applied to mixed sorts");
         }
       }
     }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 59a52a048..892b331ea 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -2208,7 +2208,7 @@ void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) {
   d_attr_handle[ str ].push_back( t );
 }
 
-void TheoryEngine::checkTheoryAssertionsWithModel() {
+void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
   for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
     Theory* theory = d_theoryTable[theoryId];
     if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
@@ -2223,7 +2223,9 @@ void TheoryEngine::checkTheoryAssertionsWithModel() {
           ss << theoryId << " has an asserted fact that the model doesn't satisfy." << endl
              << "The fact: " << assertion << endl
              << "Model value: " << val << endl;
-          InternalError(ss.str());
+	  if(hardFailure) {
+	    InternalError(ss.str());
+	  }
         }
       }
     }
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7dd3f57a6..3ae0b840b 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -883,7 +883,7 @@ public:
    * Check that the theory assertions are satisfied in the model.
    * This function is called from the smt engine's checkModel routine.
    */
-  void checkTheoryAssertionsWithModel();
+  void checkTheoryAssertionsWithModel(bool hardFailure);
 
 private:
   IntStat d_arithSubstitutionsAdded;