mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

fix build break

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-06-24 07:40:23 +02:00 • committed by Christoph M. Wintersteiger
parent 1544105bd5
commit 6bf87083ef
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/test/qe_arith.cpp
View file

@ -62,7 +62,7 @@ static void test(char const *ex) {
app_ref_vector vars(m);
expr_ref_vector lits(m);
vars.push_back(m.mk_const(symbol("x"), a.mk_real()));
qe::flatten_and(fml, lits);
flatten_and(fml, lits);
smt::context ctx(m, params);
ctx.assert_expr(fml);
@ -89,7 +89,7 @@ static void test2(char const *ex) {
vars.push_back(m.mk_const(symbol("x"), a.mk_real()));
vars.push_back(m.mk_const(symbol("y"), a.mk_real()));
vars.push_back(m.mk_const(symbol("z"), a.mk_real()));
qe::flatten_and(fml, lits);
flatten_and(fml, lits);
smt::context ctx(m, params);
ctx.push();