mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +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
parent 108d76270e
commit c3e666bc44
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); app_ref_vector vars(m);
expr_ref_vector lits(m); expr_ref_vector lits(m);
vars.push_back(m.mk_const(symbol("x"), a.mk_real())); 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); smt::context ctx(m, params);
ctx.assert_expr(fml); 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("x"), a.mk_real()));
vars.push_back(m.mk_const(symbol("y"), 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())); 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); smt::context ctx(m, params);
ctx.push(); ctx.push();