summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2017-11-05 11:44:21 -0600
committerGitHub <noreply@github.com>2017-11-05 11:44:21 -0600
commitbfeedc822f39875c7d54dac0a744a63c5dc838bd (patch)
treee40b13a5763652db656fad133779c61e79a03d40 /src/parser
parent2ef8fe2eefaecdb62653d36c88169fe906512b9d (diff)
Make higher-order a flag in logic info. (#1318)
* Make higher-order a flag in logic info. * Format * Minor * Format
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/smt2/smt2.cpp6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 0fc3678c7..a72b0ac6e 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -381,14 +381,16 @@ void Smt2::setLogic(std::string name) {
} else {
d_logic = name;
}
-
- // if sygus is enabled, we must enable UF, datatypes and integer arithmetic
+
+ // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and
+ // higher-order
if(sygus()) {
// get unlocked copy, modify, copy and relock
LogicInfo log(d_logic.getUnlockedCopy());
log.enableTheory(theory::THEORY_UF);
log.enableTheory(theory::THEORY_DATATYPES);
log.enableIntegers();
+ log.enableHigherOrder();
d_logic = log;
d_logic.lock();
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback