From ff788863577dbc8d15a584d869f543773ce0ff1d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 6 Oct 2014 14:48:14 -0400 Subject: [PATCH] Print array constants in SMT-LIB models with new syntax. --- src/printer/smt2/smt2_printer.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b415c6b19..5dc5cb7ee 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -194,7 +194,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::STORE_ALL: { ArrayStoreAll asa = n.getConst(); - out << "(__array_store_all__ " << asa.getType() << " " << asa.getExpr() << ")"; + out << "((as const " << asa.getType() << ") " << asa.getExpr() << ")"; break; } @@ -588,7 +588,6 @@ static string smtKindString(Kind k) throw() { // arrays theory case kind::SELECT: return "select"; case kind::STORE: return "store"; - case kind::STORE_ALL: return "__array_store_all__"; case kind::ARRAY_TYPE: return "Array"; // bv theory -- 2.30.2