mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
merged
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
commit
b7f636984e
|
@ -306,8 +306,7 @@ lbool interpolant_provider_impl::get_interpolant(expr * f1, expr * f2, expr_ref&
|
|||
return l_undef;
|
||||
}
|
||||
|
||||
smt_params dummy_params;
|
||||
cmd_context cctx(&dummy_params, false, &m);
|
||||
cmd_context cctx(false, &m);
|
||||
for_each_expr(used_symbol_inserter(cctx), f1);
|
||||
|
||||
parse_smt2_commands(cctx, std::istringstream(res_text), false);
|
||||
|
|
Loading…
Reference in a new issue