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

fix #5304

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-29 08:06:06 -07:00
parent 15916091d1
commit 56b47fa956
2 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/model/array_factory.cpp
View file

@ -134,8 +134,9 @@ expr * array_factory::get_fresh_value(sort * s) {
sort * range = get_array_range(s); sort * range = get_array_range(s);
expr* range_val = nullptr; expr* range_val = nullptr;
if (!m_recursive_fresh) { if (!m_ranges.contains(range)) {
flet<bool> _recursive(m_recursive_fresh, true); ptr_vector<sort>::scoped_stack _s(m_ranges);
m_ranges.push_back(range);
range_val = m_model.get_fresh_value(range); range_val = m_model.get_fresh_value(range);
if (range_val != nullptr) { if (range_val != nullptr) {
// easy case // easy case

2
src/model/array_factory.h
View file

@ -28,7 +28,7 @@ class array_factory : public struct_factory {
expr * mk_array_interp(sort * s, func_interp * & fi); expr * mk_array_interp(sort * s, func_interp * & fi);
void get_some_args_for(sort * s, ptr_buffer<expr> & args); void get_some_args_for(sort * s, ptr_buffer<expr> & args);
bool mk_two_diff_values_for(sort * s); bool mk_two_diff_values_for(sort * s);
bool m_recursive_fresh { false }; ptr_vector<sort> m_ranges;
public: public:
array_factory(ast_manager & m, model_core & md); array_factory(ast_manager & m, model_core & md);