diff options
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 5 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 7 |
2 files changed, 8 insertions, 4 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 8f433256d..42dfea308 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -702,8 +702,9 @@ void CvcPrinter::toStreamNode(std::ostream& out, op << "@"; opType = INFIX; break; - case kind::BITVECTOR_PLUS: { - // This interprets a BITVECTOR_PLUS as a bvadd in SMT-LIB + case kind::BITVECTOR_ADD: + { + // This interprets a BITVECTOR_ADD as a bvadd in SMT-LIB Assert(n.getType().isBitVector()); unsigned numc = n.getNumChildren()-2; unsigned child = 0; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 72d7fca89..2b1f16931 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -753,7 +753,10 @@ void Smt2Printer::toStream(std::ostream& out, case kind::BITVECTOR_XNOR: out << "bvxnor "; break; case kind::BITVECTOR_COMP: out << "bvcomp "; break; case kind::BITVECTOR_MULT: out << "bvmul "; forceBinary = true; break; - case kind::BITVECTOR_PLUS: out << "bvadd "; forceBinary = true; break; + case kind::BITVECTOR_ADD: + out << "bvadd "; + forceBinary = true; + break; case kind::BITVECTOR_SUB: out << "bvsub "; break; case kind::BITVECTOR_NEG: out << "bvneg "; break; case kind::BITVECTOR_UDIV: out << "bvudiv "; break; @@ -1157,7 +1160,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::BITVECTOR_XNOR: return "bvxnor"; case kind::BITVECTOR_COMP: return "bvcomp"; case kind::BITVECTOR_MULT: return "bvmul"; - case kind::BITVECTOR_PLUS: return "bvadd"; + case kind::BITVECTOR_ADD: return "bvadd"; case kind::BITVECTOR_SUB: return "bvsub"; case kind::BITVECTOR_NEG: return "bvneg"; case kind::BITVECTOR_UDIV: return "bvudiv"; |