From 21759e5eb27fdf1dbdceca27b00dcf0b3683ce88 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Jul 2017 08:59:12 -0700 Subject: [PATCH] fixes #1172 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/interpolant_cmds.cpp | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp index 53da91d1e..de79dbc52 100644 --- a/src/cmd_context/interpolant_cmds.cpp +++ b/src/cmd_context/interpolant_cmds.cpp @@ -46,20 +46,20 @@ static void show_interpolant_and_maybe_check(cmd_context & ctx, m_params.set_bool("flat", true); th_rewriter s(ctx.m(), m_params); + expr_ref_vector exprs(ctx.m()); + sort_ref_vector domain(ctx.m()); for(unsigned i = 0; i < interps.size(); i++){ - expr_ref r(ctx.m()); proof_ref pr(ctx.m()); s(to_expr(interps[i]),r,pr); - - ctx.regular_stream() << mk_pp(r.get(), ctx.m()) << std::endl; -#if 0 - ast_smt_pp pp(ctx.m()); - pp.set_logic(ctx.get_logic().str().c_str()); - pp.display_smt2(ctx.regular_stream(), to_expr(interps[i])); - ctx.regular_stream() << std::endl; -#endif + exprs.push_back(r); + domain.push_back(ctx.m().mk_bool_sort()); } + func_decl_ref fn(ctx.m()); + fn = ctx.m().mk_func_decl(symbol("interpolants"), domain.size(), domain.c_ptr(), ctx.m().mk_bool_sort()); + expr_ref tmp(ctx.m()); + tmp = ctx.m().mk_app(fn, exprs.size(), exprs.c_ptr()); + ctx.regular_stream() << tmp << "\n"; s.cleanup();