From 4a014a12d7f72c4f73dfbee8c9f62868e920bc15 Mon Sep 17 00:00:00 2001
From: Martin <martin.brain@diffblue.com>
Date: Thu, 14 Sep 2017 04:51:50 +0100
Subject: 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.
---
 src/theory/theory_engine.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/theory/theory_engine.h')

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;
-- 
cgit v1.2.3