We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
2 parents f0c59b5 + 4b3d775 commit e754de7Copy full SHA for e754de7
src/solvers/smt2/smt2_solver.cpp
@@ -167,9 +167,7 @@ void smt2_solvert::command(const std::string &c)
167
// this is a command that Z3 appears to implement
168
exprt e=expression();
169
if(e.is_not_nil())
170
- {
171
- std::cout << e.pretty() << '\n'; // need to do an 'smt2_format'
172
- }
+ std::cout << smt2_format(e) << '\n';
173
}
174
else if(c == "get-value")
175
{
@@ -237,7 +235,7 @@ void smt2_solvert::command(const std::string &c)
237
235
const symbol_tablet symbol_table;
238
236
const namespacet ns(symbol_table);
239
exprt e_simplified=simplify_expr(e, ns);
240
241
242
243
#if 0
0 commit comments