summaryrefslogtreecommitdiff
path: root/src/printer/smt2/smt2_printer.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r--src/printer/smt2/smt2_printer.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 9edc73acd..0c0c4c3a8 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -545,7 +545,7 @@ void Smt2Printer::toStream(std::ostream& out,
case kind::MATCH_CASE:
// do nothing
break;
- case kind::CHOICE: out << smtKindString(k, d_variant) << " "; break;
+ case kind::WITNESS: out << smtKindString(k, d_variant) << " "; break;
// arith theory
case kind::PLUS:
@@ -1032,7 +1032,7 @@ static string smtKindString(Kind k, Variant v)
case kind::LAMBDA:
return "lambda";
case kind::MATCH: return "match";
- case kind::CHOICE: return "choice";
+ case kind::WITNESS: return "witness";
// arith theory
case kind::PLUS: return "+";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback