summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/macros.cpp
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-10-08 20:16:58 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2014-10-14 16:41:17 -0400
commitef000094d2d6a024c7eac490b241259b38e07225 (patch)
tree395250d07c9e589b1ba42316516deddfe1486018 /src/theory/quantifiers/macros.cpp
parent7df24c61c7998e1485ab75219078deaf1455bd71 (diff)
Context-dependent expr attributes are now attached to a specific SmtEngine, and the SAT context is owned by the SmtEngine.
Diffstat (limited to 'src/theory/quantifiers/macros.cpp')
-rw-r--r--src/theory/quantifiers/macros.cpp1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 7321e22b4..81cd5948a 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -24,7 +24,6 @@ using namespace std;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
using namespace CVC4::kind;
-using namespace CVC4::context;
bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback