mirror of
https://github.com/Z3Prover/z3
synced 2026-02-12 11:54:07 +00:00
fix another regression by Nuno's changes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
850cc3e120
commit
e6c05d55a7
1 changed files with 1 additions and 0 deletions
|
|
@ -385,6 +385,7 @@ namespace qe {
|
|||
// They are sorted by size, so we project the largest variables first to avoid
|
||||
// renaming variables.
|
||||
for (unsigned i = vars.size(); i-- > 0;) {
|
||||
new_result.reset();
|
||||
ex.project(vars[i], result.size(), result.data(), new_result);
|
||||
TRACE(qe, display_project(tout, vars[i], result, new_result););
|
||||
result.swap(new_result);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue