mirror of
https://github.com/Z3Prover/z3
synced 2025-07-17 01:46:39 +00:00
string-integer integration in free var gen
This commit is contained in:
parent
91d82956b2
commit
1520760a04
1 changed files with 4 additions and 5 deletions
|
@ -5302,13 +5302,12 @@ void theory_str::process_free_var(std::map<expr*, int> & freeVar_map) {
|
||||||
}
|
}
|
||||||
|
|
||||||
if (standAlone) {
|
if (standAlone) {
|
||||||
// TODO
|
rational len_value;
|
||||||
// int lenValue = getLenValue(freeVar);
|
bool len_value_exists = get_len_value(freeVar, len_value);
|
||||||
int lenValue = -1;
|
if (len_value_exists) {
|
||||||
if (lenValue != -1) {
|
|
||||||
leafVarSet.insert(freeVar);
|
leafVarSet.insert(freeVar);
|
||||||
} else {
|
} else {
|
||||||
aloneVars[lenValue].insert(freeVar);
|
aloneVars[-1].insert(freeVar);
|
||||||
}
|
}
|
||||||
} else {
|
} else {
|
||||||
leafVarSet.insert(freeVar);
|
leafVarSet.insert(freeVar);
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue