summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.h
diff options
context:
space:
mode:
authorClark Barrett <barrett@cs.nyu.edu>2012-05-02 00:44:40 +0000
committerClark Barrett <barrett@cs.nyu.edu>2012-05-02 00:44:40 +0000
commit8ef2015de66fc409a2a2958b9452c0c9b1456ee3 (patch)
tree353b4a9d3163388aa6aef1c92aa0de5077888337 /src/theory/theory_engine.h
parent97555307af3415d6fbbac3fc9dccdafec51056b7 (diff)
Changing d_sharedTermsExist to logicInfo.isSharingEnabled()
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r--src/theory/theory_engine.h5
1 files changed, 0 insertions, 5 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e353850aa..28a1000f1 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -257,11 +257,6 @@ class TheoryEngine {
context::CDO<bool> d_inConflict;
/**
- * Does the context contain terms shared among multiple theories.
- */
- bool d_sharedTermsExist;
-
- /**
* Explain the equality literals and push all the explaining literals
* into the builder. All the non-equality literals are pushed to the
* builder.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback