mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

fix #3141

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-05 07:57:21 +01:00
parent 76d91f7d2b
commit 153d0661fe
3 changed files with 51 additions and 57 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_model_generator.cpp
View file

@ -318,7 +318,7 @@ namespace smt {
for (source const& curr : sources) {
if (curr.is_fresh_value()) {
sort * s = curr.get_value()->get_sort();
TRACE("model_fresh_bug", tout << curr << " : " << mk_pp(s, m) << "\n";);
TRACE("model_fresh_bug", tout << curr << " : " << mk_pp(s, m) << " " << curr.get_value()->get_value() << "\n";);
expr * val = m_model->get_fresh_value(s);
TRACE("model_fresh_bug", tout << curr << " := #" << (val == nullptr ? UINT_MAX : val->get_id()) << "\n";);
m_asts.push_back(val);

2
src/smt/theory_array_base.cpp
View file

@ -995,6 +995,8 @@ namespace smt {
// IMPORTANT:
// The implementation should not assume a fresh value is created for
// the else_val if the range is finite
TRACE("array", tout << mk_pp(n->get_owner(), get_manager()) << " " << mk_pp(range, get_manager()) << " " << range->is_infinite() << "\n";);
if (range->is_infinite())
else_val = TAG(void*, m.mk_extra_fresh_value(range), 1);
else