summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/macros.cpp
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2017-08-14 15:32:23 -0700
committerGitHub <noreply@github.com>2017-08-14 15:32:23 -0700
commit7b8531e83dd4c95a5b0eaa4927da5228c6942b7c (patch)
treedff858c76d88a0f0534daad060fa92b6b9c0f6c5 /src/theory/quantifiers/macros.cpp
parent2addacac33a9f0d28462121dfac5a1392470d60d (diff)
Move function defns from smt_engine_scope.h to cpp (#216)
Additionally, this commit removes unnecessary includes, adds includes to smt_engine.h in files that require it and removes s_smtEngine_current from smt_engine_scope.h.
Diffstat (limited to 'src/theory/quantifiers/macros.cpp')
-rw-r--r--src/theory/quantifiers/macros.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 6b071f8f7..a9fad80ae 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -21,6 +21,7 @@
#include "options/quantifiers_modes.h"
#include "options/quantifiers_options.h"
#include "proof/proof_manager.h"
+#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/trigger.h"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback