mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fix E instantiation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-11 17:10:47 -08:00
parent 74cfcc4730
commit 12819640b7
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/fd_solver/smtfd_solver.cpp
View file

@ -1437,10 +1437,10 @@ namespace smtfd {
unsigned sz = q->get_num_decls(); unsigned sz = q->get_num_decls();
vars.resize(sz, nullptr); vars.resize(sz, nullptr);
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
vars[sz - i - 1] = m.mk_fresh_const(q->get_decl_name(i), q->get_decl_sort(i)); vars[i] = m.mk_fresh_const(q->get_decl_name(i), q->get_decl_sort(i));
} }
var_subst subst(m); var_subst subst(m);
expr_ref body = subst(tmp, vars.size(), vars.c_ptr()); expr_ref body = subst(q->get_expr(), vars.size(), vars.c_ptr());
if (is_exists(q)) { if (is_exists(q)) {
body = m.mk_implies(q, body); body = m.mk_implies(q, body);
} }