mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fix compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d66db280a8
commit
bd92797663
|
@ -48,7 +48,7 @@ static void tst1() {
|
|||
SASSERT(v1.size() == v2.size());
|
||||
if (v1.size() > 0) {
|
||||
unsigned idx = rand()%v1.size();
|
||||
SASSERT(v1.get(idx) == v2[idx]);
|
||||
VERIFY(v1.get(idx) == v2[idx]);
|
||||
}
|
||||
}
|
||||
else if (op <= 5) {
|
||||
|
|
|
@ -133,7 +133,7 @@ public:
|
|||
params[0] = parameter(2);
|
||||
ar = m_manager.mk_app(m_fid, OP_REPEAT, 1, params, 1, es);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT(((a64 << 32) | a64) == u64(e.get()));
|
||||
VERIFY(((a64 << 32) | a64) == u64(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BREDOR, e1.get());
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
|
@ -163,11 +163,11 @@ public:
|
|||
|
||||
ar = m_manager.mk_app(m_fid, OP_BIT0);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT(!bit2bool(e.get()));
|
||||
VERIFY(!bit2bool(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BIT1);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT(bit2bool(e.get()));
|
||||
VERIFY(bit2bool(e.get()));
|
||||
|
||||
}
|
||||
|
||||
|
@ -187,113 +187,113 @@ public:
|
|||
|
||||
ar = m_manager.mk_app(m_fid, OP_BADD, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((a + b) == u32(e.get()));
|
||||
VERIFY((a + b) == u32(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BSUB, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((a - b) == u32(e.get()));
|
||||
VERIFY((a - b) == u32(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BMUL, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((a * b) == u32(e.get()));
|
||||
VERIFY((a * b) == u32(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BAND, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((a & b) == u32(e.get()));
|
||||
VERIFY((a & b) == u32(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BOR, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((a | b) == u32(e.get()));
|
||||
VERIFY((a | b) == u32(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BNOR, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT(~(a | b) == u32(e.get()));
|
||||
VERIFY(~(a | b) == u32(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BXOR, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((a ^ b) == u32(e.get()));
|
||||
VERIFY((a ^ b) == u32(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BXNOR, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((~(a ^ b)) == u32(e.get()));
|
||||
VERIFY((~(a ^ b)) == u32(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BNAND, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((~(a & b)) == u32(e.get()));
|
||||
VERIFY((~(a & b)) == u32(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_ULEQ, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((a <= b) == ast2bool(e.get()));
|
||||
VERIFY((a <= b) == ast2bool(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_UGEQ, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((a >= b) == ast2bool(e.get()));
|
||||
VERIFY((a >= b) == ast2bool(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_ULT, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((a < b) == ast2bool(e.get()));
|
||||
VERIFY((a < b) == ast2bool(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_UGT, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((a > b) == ast2bool(e.get()));
|
||||
VERIFY((a > b) == ast2bool(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_SLEQ, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((sa <= sb) == ast2bool(e.get()));
|
||||
VERIFY((sa <= sb) == ast2bool(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_SGEQ, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((sa >= sb) == ast2bool(e.get()));
|
||||
VERIFY((sa >= sb) == ast2bool(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_SLT, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((sa < sb) == ast2bool(e.get()));
|
||||
VERIFY((sa < sb) == ast2bool(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_SGT, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((sa > sb) == ast2bool(e.get()));
|
||||
VERIFY((sa > sb) == ast2bool(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BSHL, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT(((b>=32)?0:(a << b)) == u32(e.get()));
|
||||
VERIFY(((b>=32)?0:(a << b)) == u32(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BLSHR, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT(((b>=32)?0:(a >> b)) == u32(e.get()));
|
||||
VERIFY(((b>=32)?0:(a >> b)) == u32(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BASHR, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
|
||||
std::cout << "compare: " << sa << " >> " << b << " = " << (sa >> b) << " with " << i32(e.get()) << "\n";
|
||||
SASSERT(b >= 32 || ((sa >> b) == i32(e.get())));
|
||||
VERIFY(b >= 32 || ((sa >> b) == i32(e.get())));
|
||||
|
||||
if (b != 0) {
|
||||
ar = m_manager.mk_app(m_fid, OP_BSDIV, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((sa / sb) == i32(e.get()));
|
||||
VERIFY((sa / sb) == i32(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BUDIV, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((a / b) == u32(e.get()));
|
||||
VERIFY((a / b) == u32(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BSREM, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
//SASSERT((sa % sb) == i32(e.get()));
|
||||
//VERIFY((sa % sb) == i32(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BUREM, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((a % b) == u32(e.get()));
|
||||
VERIFY((a % b) == u32(e.get()));
|
||||
|
||||
// TBD: BSMOD.
|
||||
}
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_CONCAT, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT(((a64 << 32) | b64) == u64(e.get()));
|
||||
VERIFY(((a64 << 32) | b64) == u64(e.get()));
|
||||
|
||||
ar = m_manager.mk_app(m_fid, OP_BCOMP, 2, e1e2);
|
||||
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
|
||||
SASSERT((a == b) == bit2bool(e.get()));
|
||||
VERIFY((a == b) == bit2bool(e.get()));
|
||||
}
|
||||
|
||||
void test() {
|
||||
|
|
|
@ -38,7 +38,7 @@ void tst_check_assumptions()
|
|||
|
||||
expr * npE = np.get();
|
||||
lbool res1 = ctx.check(1, &npE);
|
||||
SASSERT(res1==l_true);
|
||||
VERIFY(res1 == l_true);
|
||||
|
||||
ctx.assert_expr(npE);
|
||||
|
||||
|
|
|
@ -14,6 +14,35 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
using namespace datalog;
|
||||
|
||||
|
||||
void tst_dl_context() {
|
||||
symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2") };
|
||||
|
||||
return;
|
||||
|
||||
#if 0
|
||||
const unsigned rel_cnt = sizeof(relations)/sizeof(symbol);
|
||||
const char * test_file = "c:\\tvm\\src\\benchmarks\\datalog\\t0.datalog";
|
||||
|
||||
params_ref params;
|
||||
for(unsigned rel_index=0; rel_index<rel_cnt; rel_index++) {
|
||||
params.set_sym("default_relation", relations[rel_index]);
|
||||
for(int eager_checking=1; eager_checking>=0; eager_checking--) {
|
||||
params.set_bool("eager_emptiness_checking", eager_checking!=0);
|
||||
|
||||
std::cerr << "Testing " << relations[rel_index] << "\n";
|
||||
std::cerr << "Eager emptiness checking " << (eager_checking!=0 ? "on" : "off") << "\n";
|
||||
dl_context_simple_query_test(params);
|
||||
dl_context_saturate_file(params, test_file);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
}
|
||||
|
||||
|
||||
#if 0
|
||||
|
||||
|
||||
static lbool dl_context_eval_unary_predicate(ast_manager & m, context & ctx, char const* problem_text,
|
||||
const char * pred_name) {
|
||||
parser* p = parser::create(ctx,m);
|
||||
|
@ -72,29 +101,4 @@ void dl_context_saturate_file(params_ref & params, const char * f) {
|
|||
ctx.get_rel_context()->saturate();
|
||||
std::cerr << "Done\n";
|
||||
}
|
||||
|
||||
void tst_dl_context() {
|
||||
symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2") };
|
||||
const unsigned rel_cnt = sizeof(relations)/sizeof(symbol);
|
||||
|
||||
return;
|
||||
#if 0
|
||||
const char * test_file = "c:\\tvm\\src\\benchmarks\\datalog\\t0.datalog";
|
||||
|
||||
params_ref params;
|
||||
for(unsigned rel_index=0; rel_index<rel_cnt; rel_index++) {
|
||||
params.set_sym("default_relation", relations[rel_index]);
|
||||
for(int eager_checking=1; eager_checking>=0; eager_checking--) {
|
||||
params.set_bool("eager_emptiness_checking", eager_checking!=0);
|
||||
|
||||
std::cerr << "Testing " << relations[rel_index] << "\n";
|
||||
std::cerr << "Eager emptiness checking " << (eager_checking!=0 ? "on" : "off") << "\n";
|
||||
dl_context_simple_query_test(params);
|
||||
dl_context_saturate_file(params, test_file);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
|
|
@ -40,7 +40,7 @@ void dl_query_ask_for_last_arg(context & ctx, func_decl * pred, relation_fact &
|
|||
|
||||
lbool is_sat = ctx.query(query);
|
||||
std::cerr << "@@ last arg query should succeed: " << should_be_successful << "\n";
|
||||
SASSERT(is_sat != l_undef);
|
||||
VERIFY(is_sat != l_undef);
|
||||
|
||||
relation_fact res_fact(m);
|
||||
res_fact.push_back(f.back());
|
||||
|
|
|
@ -77,6 +77,7 @@ static void dump_heap(const int_heap2 & h, std::ostream & out) {
|
|||
}
|
||||
|
||||
static void tst2() {
|
||||
(void)dump_heap;
|
||||
int_heap2 h(N);
|
||||
for (int i = 0; i < N * 10; i++) {
|
||||
if (i % 1000 == 0) std::cout << "i: " << i << std::endl;
|
||||
|
|
|
@ -44,19 +44,19 @@ static void bug_to_rational() {
|
|||
unsynch_mpq_manager mq;
|
||||
scoped_mpq r(mq);
|
||||
|
||||
double ad, rd;
|
||||
double ad = 0, rd = 0;
|
||||
|
||||
m.set(a, 0.0);
|
||||
m.to_rational(a, r);
|
||||
ad = m.to_double(a);
|
||||
rd = mq.get_double(r);
|
||||
SASSERT(ad == rd);
|
||||
VERIFY(ad == rd);
|
||||
|
||||
m.set(a, 1.0);
|
||||
m.to_rational(a, r);
|
||||
ad = m.to_double(a);
|
||||
rd = mq.get_double(r);
|
||||
SASSERT(ad == rd);
|
||||
VERIFY(ad == rd);
|
||||
|
||||
m.set(a, 1.5);
|
||||
m.to_rational(a, r);
|
||||
|
|
|
@ -35,6 +35,7 @@ static void tst1() {
|
|||
list<int> * l5 = append(r, l4, l2);
|
||||
TRACE("list", display(tout, l5->begin(), l5->end()); tout << "\n";);
|
||||
list<int> * l6 = append(r, l5, l5);
|
||||
(void) l6;
|
||||
TRACE("list", display(tout, l6->begin(), l6->end()); tout << "\n";);
|
||||
}
|
||||
|
||||
|
|
|
@ -435,7 +435,7 @@ static void tst_limits(unsigned prec) {
|
|||
bool overflow = false;
|
||||
try { m.inc(a); }
|
||||
catch (mpff_manager::overflow_exception) { overflow = true; }
|
||||
SASSERT(overflow);
|
||||
VERIFY(overflow);
|
||||
m.set_max(a);
|
||||
m.dec(a);
|
||||
SASSERT(m.eq(a, b));
|
||||
|
|
|
@ -391,7 +391,6 @@ static void tst7() {
|
|||
params_ref ps;
|
||||
reslimit rlim;
|
||||
nlsat::solver s(rlim, ps);
|
||||
anum_manager & am = s.am();
|
||||
nlsat::pmanager & pm = s.pm();
|
||||
nlsat::var x0, x1, x2, a, b, c, d;
|
||||
a = s.mk_var(false);
|
||||
|
@ -423,7 +422,7 @@ static void tst7() {
|
|||
|
||||
nlsat::literal_vector litsv(lits.size(), lits.c_ptr());
|
||||
lbool res = s.check(litsv);
|
||||
SASSERT(res == l_false);
|
||||
VERIFY(res == l_false);
|
||||
for (unsigned i = 0; i < litsv.size(); ++i) {
|
||||
s.display(std::cout, litsv[i]);
|
||||
std::cout << " ";
|
||||
|
|
|
@ -83,10 +83,10 @@ static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vector<r
|
|||
th_rw(fml2, result2, proof);
|
||||
SASSERT(m.is_true(result2) || m.is_false(result2));
|
||||
lbool res = solver.check();
|
||||
SASSERT(res == l_true);
|
||||
VERIFY(res == l_true);
|
||||
solver.assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get());
|
||||
res = solver.check();
|
||||
SASSERT(res == l_false);
|
||||
VERIFY(res == l_false);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -152,10 +152,10 @@ static void test_solver_semantics(ast_manager& m, expr_ref_vector const& vars, v
|
|||
th_rw(fml2, result2, proof);
|
||||
SASSERT(m.is_true(result2) || m.is_false(result2));
|
||||
lbool res = slv->check_sat(0,0);
|
||||
SASSERT(res == l_true);
|
||||
VERIFY(res == l_true);
|
||||
slv->assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get());
|
||||
res = slv->check_sat(0,0);
|
||||
SASSERT(res == l_false);
|
||||
VERIFY(res == l_false);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -88,6 +88,7 @@ private:
|
|||
expr_ref_vector& factors = poly.factors();
|
||||
expr_ref_vector& coefficients = poly.coefficients();
|
||||
expr_ref& coefficient = poly.coefficient();
|
||||
(void) coefficient;
|
||||
|
||||
m_rw(term);
|
||||
|
||||
|
|
|
@ -11,7 +11,6 @@ void tst_checker1() {
|
|||
ast_manager m(PGM_FINE);
|
||||
expr_ref a(m);
|
||||
proof_ref p1(m), p2(m), p3(m), p4(m);
|
||||
bool result;
|
||||
expr_ref_vector side_conditions(m);
|
||||
|
||||
a = m.mk_const(symbol("a"), m.mk_bool_sort());
|
||||
|
@ -26,8 +25,7 @@ void tst_checker1() {
|
|||
proof_checker checker(m);
|
||||
p4 = m.mk_lemma(p3.get(), m.mk_or(a.get(), m.mk_not(a.get())));
|
||||
ast_ll_pp(std::cout, m, p4.get());
|
||||
result = checker.check(p4.get(), side_conditions);
|
||||
SASSERT(result);
|
||||
VERIFY(checker.check(p4.get(), side_conditions));
|
||||
}
|
||||
|
||||
void tst_proof_checker() {
|
||||
|
|
|
@ -196,7 +196,7 @@ static void tst2() {
|
|||
// get_int64, get_uint64
|
||||
uint64 u1 = uint64_max.get_uint64();
|
||||
uint64 u2 = UINT64_MAX;
|
||||
SASSERT(u1 == u2);
|
||||
VERIFY(u1 == u2);
|
||||
std::cout << "int64_max: " << int64_max << ", INT64_MAX: " << INT64_MAX << ", int64_max.get_int64(): " << int64_max.get_int64() << ", int64_max.get_uint64(): " << int64_max.get_uint64() << "\n";
|
||||
SASSERT(int64_max.get_int64() == INT64_MAX);
|
||||
SASSERT(int64_min.get_int64() == INT64_MIN);
|
||||
|
|
|
@ -35,6 +35,7 @@ static void add_clause(sat::solver& s, random_gen& r, trail_t& t) {
|
|||
}
|
||||
|
||||
static void display_state(std::ostream& out, sat::solver& s, trail_t& t) {
|
||||
(void)t;
|
||||
s.display(out);
|
||||
}
|
||||
|
||||
|
|
|
@ -38,6 +38,7 @@ void tst_simple_parser() {
|
|||
TRACE("simple_parser", tout << mk_pp(r, m) << "\n";);
|
||||
p.parse_string("(+ x (* y x) x)", r);
|
||||
float vals[2] = { 2.0f, 3.0f };
|
||||
(void)vals;
|
||||
TRACE("simple_parser",
|
||||
tout << mk_pp(r, m) << "\n";
|
||||
tout << "val: " << eval(r, 2, vals) << "\n";);
|
||||
|
|
|
@ -129,18 +129,18 @@ static void tst_isolate_roots(polynomial_ref const & p, unsigned prec, mpbq_mana
|
|||
tout << "fourier upper: " << um.sign_variations_at(fseq, uppers[i]) << "\n";);
|
||||
unsigned fsv_lower = um.sign_variations_at(fseq, lowers[i]);
|
||||
unsigned fsv_upper = um.sign_variations_at(fseq, uppers[i]);
|
||||
SASSERT(um.eval_sign_at(q.size(), q.c_ptr(), lowers[i]) == 0 ||
|
||||
um.eval_sign_at(q.size(), q.c_ptr(), uppers[i]) == 0 ||
|
||||
VERIFY(um.eval_sign_at(q.size(), q.c_ptr(), lowers[i]) == 0 ||
|
||||
um.eval_sign_at(q.size(), q.c_ptr(), uppers[i]) == 0 ||
|
||||
// fsv_lower - fsv_upper is an upper bound for the number of roots in the interval
|
||||
// fsv_upper - fsv_upper - num_roots is even
|
||||
// Recall that num_roots == 1 in the interval.
|
||||
(fsv_lower - fsv_upper >= 1 && (fsv_lower - fsv_upper - 1) % 2 == 0));
|
||||
|
||||
(fsv_lower - fsv_upper >= 1 && (fsv_lower - fsv_upper - 1) % 2 == 0));
|
||||
|
||||
// Double checking using Descartes bounds for the interval
|
||||
// Must use square free component.
|
||||
unsigned dab = um.descartes_bound_a_b(q_sqf.size(), q_sqf.c_ptr(), bqm, lowers[i], uppers[i]);
|
||||
TRACE("upolynomial", tout << "Descartes bound: " << dab << "\n";);
|
||||
SASSERT(dab == 1);
|
||||
VERIFY(dab == 1);
|
||||
}
|
||||
}
|
||||
std::cout << "\n";
|
||||
|
@ -499,7 +499,7 @@ static void tst_refinable(polynomial_ref const & p, mpbq_manager & bqm, mpbq & a
|
|||
std::cout << "new (" << bqm.to_string(a) << ", " << bqm.to_string(b) << ")\n";
|
||||
int sign_a = um.eval_sign_at(_p.size(), _p.c_ptr(), a);
|
||||
int sign_b = um.eval_sign_at(_p.size(), _p.c_ptr(), b);
|
||||
SASSERT(sign_a != 0 && sign_b != 0 && sign_a == -sign_b);
|
||||
VERIFY(sign_a != 0 && sign_b != 0 && sign_a == -sign_b);
|
||||
}
|
||||
else {
|
||||
std::cout << "new root: " << bqm.to_string(a) << "\n";
|
||||
|
|
Loading…
Reference in a new issue