mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 04:03:39 +00:00
fix #5312
This commit is contained in:
parent
56b47fa956
commit
3024fe7baf
|
@ -293,6 +293,7 @@ namespace smt {
|
||||||
obj_map<enode, model_value_proc *> root2proc;
|
obj_map<enode, model_value_proc *> root2proc;
|
||||||
ptr_vector<enode> roots;
|
ptr_vector<enode> roots;
|
||||||
ptr_vector<model_value_proc> procs;
|
ptr_vector<model_value_proc> procs;
|
||||||
|
scoped_reset _scoped_reset(*this, procs);
|
||||||
svector<source> sources;
|
svector<source> sources;
|
||||||
buffer<model_value_dependency> dependencies;
|
buffer<model_value_dependency> dependencies;
|
||||||
expr_ref_vector dependency_values(m);
|
expr_ref_vector dependency_values(m);
|
||||||
|
@ -315,7 +316,6 @@ namespace smt {
|
||||||
m_context->display(tout);
|
m_context->display(tout);
|
||||||
);
|
);
|
||||||
|
|
||||||
scoped_reset _scoped_reset(*this, procs);
|
|
||||||
|
|
||||||
for (source const& curr : sources) {
|
for (source const& curr : sources) {
|
||||||
if (curr.is_fresh_value()) {
|
if (curr.is_fresh_value()) {
|
||||||
|
|
Loading…
Reference in a new issue