mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

fix array regressions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-03 13:22:12 -08:00
parent 8b261df77a
commit 6c331279ae
3 changed files with 1 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/array_decl_plugin.cpp
View file

@ -127,7 +127,6 @@ func_decl * array_decl_plugin::mk_const(sort * s, unsigned arity, sort * const *
return nullptr; return nullptr;
} }
if (!m_manager->compatible_sorts(get_array_range(s), domain[0])) { if (!m_manager->compatible_sorts(get_array_range(s), domain[0])) {
SASSERT(false);
m_manager->raise_exception("invalid const array definition, sort mismatch between array range and argument"); m_manager->raise_exception("invalid const array definition, sort mismatch between array range and argument");
return nullptr; return nullptr;
} }

5
src/ast/array_decl_plugin.h
View file

@ -180,11 +180,6 @@ public:
parameter param(s); parameter param(s);
return m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, &param, 1, &v); return m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, &param, 1, &v);
} }
app * mk_const_array(unsigned n, sort * const* s, expr * v) {
vector<parameter> ps;
for (unsigned i = 0; i < n; ++i) ps.push_back(parameter(s[i]));
return m_manager.mk_app(m_fid, OP_CONST_ARRAY, n, ps.c_ptr(), 1, &v);
}
app * mk_empty_set(sort * s) { app * mk_empty_set(sort * s) {
return mk_const_array(s, m_manager.mk_false()); return mk_const_array(s, m_manager.mk_false());
} }

2
src/cmd_context/eval_cmd.cpp
View file

@ -71,7 +71,7 @@ public:
expr_ref r(ctx.m()); expr_ref r(ctx.m());
unsigned timeout = m_params.get_uint("timeout", UINT_MAX); unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
unsigned rlimit = m_params.get_uint("rlimit", 0); unsigned rlimit = m_params.get_uint("rlimit", 0);
md->compress(); // md->compress();
model_evaluator ev(*(md.get()), m_params); model_evaluator ev(*(md.get()), m_params);
ev.set_solver(alloc(th_solver, ctx)); ev.set_solver(alloc(th_solver, ctx));
cancel_eh<reslimit> eh(ctx.m().limit()); cancel_eh<reslimit> eh(ctx.m().limit());