mirror of
https://github.com/Z3Prover/z3
synced 2025-07-25 21:57:00 +00:00
fix the test-z3 build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
0e71a9d11c
commit
126e06b8b6
1 changed files with 1 additions and 1 deletions
|
@ -319,7 +319,7 @@ static void project(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned
|
||||||
static void project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned num, nlsat::literal const* lits) {
|
static void project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned num, nlsat::literal const* lits) {
|
||||||
std::cout << "Project ";
|
std::cout << "Project ";
|
||||||
nlsat::scoped_literal_vector result(s);
|
nlsat::scoped_literal_vector result(s);
|
||||||
ex(num, lits, result);
|
ex.main_operator(num, lits, result);
|
||||||
std::cout << "(or";
|
std::cout << "(or";
|
||||||
for (auto l : result) {
|
for (auto l : result) {
|
||||||
s.display(std::cout << " ", l);
|
s.display(std::cout << " ", l);
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue