mirror of
https://github.com/Z3Prover/z3
synced 2025-04-04 16:44:07 +00:00
replace Exists by ForAll in the mathematica lemmas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
39df8999c8
commit
e4897fff00
|
@ -3736,7 +3736,7 @@ namespace nlsat {
|
|||
}
|
||||
}
|
||||
|
||||
out << "Resolve[Exists[{";
|
||||
out << "Resolve[ForAll[{";
|
||||
bool first = true;
|
||||
for (var x = 0; x < num_vars(); x++) {
|
||||
if (used_vars[x]) {
|
||||
|
|
Loading…
Reference in a new issue