summaryrefslogtreecommitdiff
path: root/src/parser/smt2
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2')
-rw-r--r--src/parser/smt2/Smt2.g4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 00f2e944d..75df38637 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2307,8 +2307,8 @@ termAtomic[CVC4::api::Term& atomTerm]
sortSymbol[type,CHECK_DECLARED]
sortSymbol[type2,CHECK_DECLARED]
{
- api::Term v1 = SOLVER->mkVar(api::Sort(type), "_emp1");
- api::Term v2 = SOLVER->mkVar(api::Sort(type2), "_emp2");
+ api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1");
+ api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2");
atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback