From 4b3d7755a39c81bf12cc5f979f9fd586576a80a2 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 28 Nov 2018 12:23:38 -0800 Subject: [PATCH] smt2_solver: use smt2_format instead of .pretty() --- src/solvers/smt2/smt2_solver.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/solvers/smt2/smt2_solver.cpp b/src/solvers/smt2/smt2_solver.cpp index eaad9d8a00e..73c274551d3 100644 --- a/src/solvers/smt2/smt2_solver.cpp +++ b/src/solvers/smt2/smt2_solver.cpp @@ -167,9 +167,7 @@ void smt2_solvert::command(const std::string &c) // this is a command that Z3 appears to implement exprt e=expression(); if(e.is_not_nil()) - { - std::cout << e.pretty() << '\n'; // need to do an 'smt2_format' - } + std::cout << smt2_format(e) << '\n'; } else if(c == "get-value") { @@ -237,7 +235,7 @@ void smt2_solvert::command(const std::string &c) const symbol_tablet symbol_table; const namespacet ns(symbol_table); exprt e_simplified=simplify_expr(e, ns); - std::cout << e.pretty() << '\n'; // need to do an 'smt2_format' + std::cout << smt2_format(e) << '\n'; } } #if 0