Floating point symfpu support (#1093)

Changes needed for the bit-blasting floating-point solver which are outside of it's area and / or applicable independently.

1 files changed, 4 insertions, 2 deletions

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());
+	  }
         }
       }
     }