mirror of
https://github.com/Z3Prover/z3
synced 2025-08-23 11:37:54 +00:00
filter out terms that are not solved
This commit is contained in:
parent
f89e133d52
commit
dd211bade9
2 changed files with 8 additions and 5 deletions
|
@ -995,9 +995,11 @@ extern "C" {
|
|||
_terms.reset();
|
||||
_guards.reset();
|
||||
for (solver::solution const& s : solutions) {
|
||||
if (!s.term)
|
||||
continue;
|
||||
_vars.push_back(s.var);
|
||||
_terms.push_back(s.term);
|
||||
_guards.push_back(s.guard);
|
||||
_guards.push_back(s.guard ? s.guard : m.mk_true());
|
||||
}
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue