diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index bd8266dc2..40ecbd8c7 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -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();