summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r--src/theory/theory_engine.h5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0b1afe748..cb0158dfe 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -254,7 +254,8 @@ public:
* Check all (currently-active) theories for conflicts.
* @param effort the effort level to use
*/
- inline void check(theory::Theory::Effort effort) {
+ inline bool check(theory::Theory::Effort effort) {
+ bool ok = true;
try {
//d_bool.check(effort);
d_uf.check(effort);
@@ -263,7 +264,9 @@ public:
//d_bv.check(effort);
} catch(const theory::Interrupted&) {
Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
+ ok = false;
}
+ return ok;
}
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback