mirror of
https://github.com/Z3Prover/z3
synced 2025-08-09 04:31:24 +00:00
fix model generation for theory_str
This commit is contained in:
parent
1520760a04
commit
fd968783a5
1 changed files with 1 additions and 3 deletions
|
@ -44,9 +44,7 @@ namespace smt {
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
virtual expr * get_fresh_value(sort * s) {
|
virtual expr * get_fresh_value(sort * s) {
|
||||||
// TODO this may be causing crashes in model gen? investigate
|
return m_util.mk_fresh_string();
|
||||||
//return m_util.mk_fresh_string();
|
|
||||||
NOT_IMPLEMENTED_YET();
|
|
||||||
}
|
}
|
||||||
virtual void register_value(expr * n) { /* Ignore */ }
|
virtual void register_value(expr * n) { /* Ignore */ }
|
||||||
};
|
};
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue