summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r--src/parser/smt2/smt2.cpp2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 4d3062d81..9fd6588bb 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -60,6 +60,8 @@ void Smt2::addTheory(Parser& parser, Theory theory) {
switch(theory) {
case THEORY_CORE:
parser.defineType("Bool", parser.getExprManager()->booleanType());
+ parser.defineVar("true", parser.getExprManager()->mkConst(true));
+ parser.defineVar("false", parser.getExprManager()->mkConst(false));
parser.addOperator(kind::AND);
parser.addOperator(kind::EQUAL);
parser.addOperator(kind::IFF);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback