From 9e6f9c0a91d916d8f92bc0954c250d8441f1c6ba Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Tue, 28 Jan 2014 23:14:52 +0100
Subject: [PATCH] Ensure check_satisfiability is called in onestep()
Avoid that the actuall reasoner call is removed together with the
assert() on the use of heavy compiler optimization flags.
---
GMLMIP-0.1/formulas/formula.cpp | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/GMLMIP-0.1/formulas/formula.cpp b/GMLMIP-0.1/formulas/formula.cpp
index 5493548..dc58133 100644
--- a/GMLMIP-0.1/formulas/formula.cpp
+++ b/GMLMIP-0.1/formulas/formula.cpp
@@ -55,7 +55,8 @@ vector<SatisfyingAssignment> Formula<ModalValueType>::onestep() {
rulechildren.clear();
bool backup_rek = recursive_satisfiability_check;
recursive_satisfiability_check = false;
- assert(false == check_satisfiability(bdd_rep));
+ bool isSat = check_satisfiability(bdd_rep);
+ assert(isSat == false);
recursive_satisfiability_check = backup_rek;
vector<SatisfyingAssignment> ret = rulechildren;
rulechildren.clear();
--
GitLab