diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-29 13:58:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-29 13:58:09 -0500 |
commit | 90eddb069c3c9abf96719ac20aff45b44af86207 (patch) | |
tree | 5e9b48565fdcc33ecbc094ae5e14101e6e4ccb3c /src/parser/smt2/smt2.cpp | |
parent | 3aba99657b39ccc0ab400c7ed9778673a3acddd7 (diff) |
Support get-abduct smt2 command (#3122)
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 278f2bdfd..752bf58b4 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -674,11 +674,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) } // get unlocked copy, modify, copy and relock LogicInfo log(d_logic.getUnlockedCopy()); - log.enableQuantifiers(); - log.enableTheory(theory::THEORY_UF); - log.enableTheory(theory::THEORY_DATATYPES); - log.enableIntegers(); - log.enableHigherOrder(); + // enable everything needed for sygus + log.enableSygus(); d_logic = log; d_logic.lock(); } |