mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

Make terms that are internalized on the fly relevant

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2021-09-14 15:46:58 +00:00
parent 8e69f76784
commit 00e8ea7962
No known key found for this signature in database
GPG key ID: BCF6360F86294467
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_fpa.cpp
View file

@ -38,7 +38,7 @@ namespace smt {
{ {
params_ref p; params_ref p;
p.set_bool("arith_lhs", true); p.set_bool("arith_lhs", true);
m_th_rw.updt_params(p); m_th_rw.updt_params(p);
} }
theory_fpa::~theory_fpa() theory_fpa::~theory_fpa()
@ -284,6 +284,9 @@ namespace smt {
} }
default: /* ignore */; default: /* ignore */;
} }
if (!ctx.relevancy())
relevant_eh(term);
} }
return true; return true;
@ -623,7 +626,7 @@ namespace smt {
bv2fp.convert_min_max_specials(&mdl, &new_model, seen); bv2fp.convert_min_max_specials(&mdl, &new_model, seen);
bv2fp.convert_uf2bvuf(&mdl, &new_model, seen); bv2fp.convert_uf2bvuf(&mdl, &new_model, seen);
for (func_decl* f : seen) for (func_decl* f : seen)
mdl.unregister_decl(f); mdl.unregister_decl(f);
for (unsigned i = 0; i < new_model.get_num_constants(); i++) { for (unsigned i = 0; i < new_model.get_num_constants(); i++) {