summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-01-03 09:35:27 -0600
committerGitHub <noreply@github.com>2018-01-03 09:35:27 -0600
commit1a11e8a71812d1abbf3fb13230c233d741c81fd1 (patch)
tree81be35f5bd356ca6b234ef49e62e966e062eec24 /src/smt/smt_engine.h
parente75a0d05db7133a90ec1fc4b9178c324e910b799 (diff)
Global negate (#1466)
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r--src/smt/smt_engine.h5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index c628a1952..6d648ccda 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -241,6 +241,11 @@ class CVC4_PUBLIC SmtEngine {
*/
bool d_earlyTheoryPP;
+ /*
+ * Whether we did a global negation of the formula.
+ */
+ bool d_globalNegation;
+
/**
* Most recent result of last checkSat/query or (set-info :status).
*/
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback