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

replace old mk_value behaviour in theory_str that creates placeholders for unused terms instead of crashing

Browse source
This commit is contained in:
Murphy Berzish 2016-07-07 16:13:48 -04:00
parent 9eead64d03
commit 847a5fc1f8
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_str.cpp
View file

@ -6844,8 +6844,7 @@ model_value_proc * theory_str::mk_value(enode * n, model_generator & mg) {
TRACE("t_str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;);
// TODO make absolutely sure the reason we can't find a concrete value is because of an unassigned temporary
// e.g. for an expression like (Concat X $$_str0)
//return alloc(expr_wrapper_proc, m_strutil.mk_string("**UNUSED**"));
NOT_IMPLEMENTED_YET();
return alloc(expr_wrapper_proc, m_strutil.mk_string("**UNUSED**"));
}
}