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

z3str3: setup uninterpreted functions as though they were string variables

Browse source
This commit is contained in:
Murphy Berzish 2019-09-24 13:18:16 -04:00 committed by Nikolaj Bjorner
parent 301209cda6
commit 1c70bcee69
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_str.cpp
View file

@ -8417,7 +8417,7 @@ namespace smt {
TRACE("str", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;); TRACE("str", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;);
string_int_conversion_terms.push_back(ap); string_int_conversion_terms.push_back(ap);
m_library_aware_axiom_todo.push_back(n); m_library_aware_axiom_todo.push_back(n);
} else if (ap->get_num_args() == 0 && !u.str.is_string(ap)) { } else if (/*ap->get_num_args() == 0 &&*/ !u.str.is_string(ap)) {
// if ex is a variable, add it to our list of variables // if ex is a variable, add it to our list of variables
TRACE("str", tout << "tracking variable " << mk_ismt2_pp(ap, get_manager()) << std::endl;); TRACE("str", tout << "tracking variable " << mk_ismt2_pp(ap, get_manager()) << std::endl;);
variable_set.insert(ex); variable_set.insert(ex);