diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 327e280cf12..5dd9f60806f 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -942,3 +942,13 @@ app* bv_util::mk_int2bv(unsigned sz, expr* e) { parameter p(sz); return m_manager.mk_app(get_fid(), OP_INT2BV, 1, &p, 1, &e); } + +app* bv_util::mk_bv_rotate_left(expr* arg, unsigned n) { + parameter p(n); + return m_manager.mk_app(get_fid(), OP_ROTATE_LEFT, 1, &p, 1, &arg); +} + +app* bv_util::mk_bv_rotate_right(expr* arg, unsigned n) { + parameter p(n); + return m_manager.mk_app(get_fid(), OP_ROTATE_RIGHT, 1, &p, 1, &arg); +} \ No newline at end of file diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 89588ee0ea8..a2bb9d8138d 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -546,6 +546,11 @@ class bv_util : public bv_recognizers { app * mk_bv2int(expr* e); app * mk_int2bv(unsigned sz, expr* e); + app* mk_bv_rotate_left(expr* arg1, expr* arg2) { return m_manager.mk_app(get_fid(), OP_EXT_ROTATE_LEFT, arg1, arg2); } + app* mk_bv_rotate_right(expr* arg1, expr* arg2) { return m_manager.mk_app(get_fid(), OP_EXT_ROTATE_RIGHT, arg1, arg2); } + app* mk_bv_rotate_left(expr* arg, unsigned n); + app* mk_bv_rotate_right(expr* arg, unsigned n); + // TODO: all these binary ops commute (right?) but it'd be more logical to swap `n` & `m` in the `return` app * mk_bvsmul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_OVFL, n, m); } app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, n, m); } diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index 46b2c2183d4..6ba3d734e40 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -46,46 +46,53 @@ namespace bv { m_eval.init_fixed(m_terms.assertions()); } + std::pair sls::next_to_repair() { + app* e = nullptr; + if (!m_repair_down.empty()) { + unsigned index = m_rand(m_repair_down.size()); + e = m_terms.term(m_repair_down.elem_at(index)); + } + else if (m_repair_up.empty()) { + unsigned index = m_rand(m_repair_up.size()); + e = m_terms.term(m_repair_up.elem_at(index)); + } + return { !m_repair_down.empty(), e }; + } + lbool sls::operator()() { // init and init_eval were invoked. unsigned& n = m_stats.m_moves; n = 0; for (; n < m_config.m_max_repairs && m.inc(); ++n) { - if (!m_repair_down.empty()) { - unsigned index = m_rand(m_repair_down.size()); - unsigned expr_id = m_repair_down.elem_at(index); - auto e = m_terms.term(expr_id); - IF_VERBOSE(20, verbose_stream() << "d " << mk_bounded_pp(e, m, 1) << "\n"); - if (eval_is_correct(e)) - m_repair_down.remove(expr_id); + auto [down, e] = next_to_repair(); + if (!e) + return l_true; + IF_VERBOSE(20, verbose_stream() << (down?"d ":"u ") << mk_bounded_pp(e, m, 1) << "\n"); + if (eval_is_correct(e)) { + if (down) + m_repair_down.remove(e->get_id()); else - try_repair_down(e); + m_repair_up.remove(e->get_id()); } - else if (!m_repair_up.empty()) { - unsigned index = m_rand(m_repair_up.size()); - unsigned expr_id = m_repair_up.elem_at(index); - auto e = m_terms.term(expr_id); - IF_VERBOSE(20, verbose_stream() << "u " << mk_bounded_pp(e, m, 1) << "\n"); - if (eval_is_correct(e)) - m_repair_up.remove(expr_id); - else - try_repair_up(e); + else if (down) { + try_repair_down(e); } - else - return l_true; + else + try_repair_up(e); } return l_undef; } - bool sls::try_repair_down(app* e) { + void sls::try_repair_down(app* e) { unsigned n = e->get_num_args(); - if (n == 0) - return false; - unsigned s = m_rand(n); - for (unsigned i = 0; i < n; ++i) - if (try_repair_down(e, (i + s) % n)) - return true; - return false; + if (n > 0) { + unsigned s = m_rand(n); + for (unsigned i = 0; i < n; ++i) + if (try_repair_down(e, (i + s) % n)) + return; + } + m_repair_down.remove(e->get_id()); + m_repair_up.insert(e->get_id()); } bool sls::try_repair_down(app* e, unsigned i) { @@ -99,17 +106,16 @@ namespace bv { return was_repaired; } - bool sls::try_repair_up(app* e) { + void sls::try_repair_up(app* e) { m_repair_up.remove(e->get_id()); if (m_terms.is_assertion(e)) { m_repair_down.insert(e->get_id()); - return false; } - m_eval.repair_up(e); - for (auto p : m_terms.parents(e)) - m_repair_up.insert(p->get_id()); - - return true; + else { + m_eval.repair_up(e); + for (auto p : m_terms.parents(e)) + m_repair_up.insert(p->get_id()); + } } bool sls::eval_is_correct(app* e) { diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h index 6acaf483caf..781174aeed7 100644 --- a/src/ast/sls/bv_sls.h +++ b/src/ast/sls/bv_sls.h @@ -49,10 +49,11 @@ namespace bv { random_gen m_rand; config m_config; + std::pair next_to_repair(); bool eval_is_correct(app* e); - bool try_repair_down(app* e); - bool try_repair_up(app* e); + void try_repair_down(app* e); + void try_repair_up(app* e); bool try_repair_down(app* e, unsigned i); diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index bb54e0c556c..630e5e423f8 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -343,16 +343,9 @@ namespace bv { } }; - auto mk_rotate_left = [&](unsigned n) { + auto mk_rotate_left = [&](unsigned n) { auto& a = wval0(e->get_arg(0)); - if (n == 0 || a.bw == 1) - val.set(a.bits); - else { - for (unsigned i = a.bw - n; i < a.bw; ++i) - val.set(val.bits, i + n - a.bw, a.get(a.bits, i)); - for (unsigned i = 0; i < a.bw - n; ++i) - val.set(val.bits, i + a.bw - n, a.get(a.bits, i)); - } + VERIFY(try_repair_rotate_left(a, val, a.bw - n)); }; SASSERT(e->get_family_id() == bv.get_fid()); @@ -853,6 +846,7 @@ namespace bv { auto child = e->get_arg(i); auto ev = bval0(e); if (m.is_bool(child)) { + SASSERT(!is_fixed0(child)); auto bv = bval0(e->get_arg(1 - i)); m_eval[child->get_id()] = ev == bv; return true; @@ -863,12 +857,21 @@ namespace bv { if (ev) return a.try_set(b.bits); else { - // pick random bit to differ - for (unsigned i = 0; i < a.nw; ++i) - m_tmp[i] = a.bits[i]; - unsigned idx = m_rand(a.bw); - a.set(m_tmp, idx, !b.get(b.bits, idx)); - return a.try_set(m_tmp); + // pick random bit to differ + a.get(m_tmp); + unsigned start = m_rand(a.bw); + for (unsigned idx = 0; idx < a.bw; ++idx) { + unsigned j = (idx + start) % a.bw; + if (!a.get(a.fixed, j)) { + a.set(m_tmp, idx, !b.get(b.bits, j)); + bool r = a.try_set(m_tmp); + if (r) + return true; + a.set(m_tmp, j, b.get(b.bits, j)); + } + } + // could be due to bounds? + return false; } } return false; @@ -1107,9 +1110,9 @@ namespace bv { return false; } - bool sls_eval::try_repair_rotate_left(bvval const& e, bvval& a, unsigned n) { + bool sls_eval::try_repair_rotate_left(bvval const& e, bvval& a, unsigned n) const { // a := rotate_right(e, n) - n = (n % a.bw) - n; + n = (a.bw - n) % a.bw; for (unsigned i = a.bw - n; i < a.bw; ++i) a.set(m_tmp, i + n - a.bw, e.get(e.bits, i)); for (unsigned i = 0; i < a.bw - n; ++i) diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index 7d487ea7c61..5fa51ed178a 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -88,10 +88,9 @@ namespace bv { bool try_repair_smod(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_urem(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_srem(bvval const& e, bvval& a, bvval& b, unsigned i); - bool try_repair_rotate_left(bvval const& e, bvval& a, unsigned n); + bool try_repair_rotate_left(bvval const& e, bvval& a, unsigned n) const; bool try_repair_rotate_left(bvval const& e, bvval& a, bvval& b, unsigned i); - sls_valuation& wval0(app* e, unsigned i) { return wval0(e->get_arg(i)); } void wval1(app* e, sls_valuation& val) const; diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index e2c58a47cce..fb2c8f129ad 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -33,26 +33,27 @@ namespace bv { for (unsigned i = 0; i < nw; ++i) lo[i] = 0, hi[i] = 0, bits[i] = 0, fixed[i] = 0; for (unsigned i = bw; i < 8 * sizeof(digit_t) * nw; ++i) - set(fixed, i, true); + set(fixed, i, false); } sls_valuation::~sls_valuation() { } - bool sls_valuation::is_feasible() const { - return true; - mpn_manager m; - unsigned nb = (bw + 7) / 8; - auto c = m.compare(lo.data(), nb, hi.data(), nb); + bool sls_valuation::in_range(svector const& bits) const { + mpn_manager m; + auto c = m.compare(lo.data(), nw, hi.data(), nw); + // full range if (c == 0) return true; + // lo < hi: then lo <= bits & bits < hi if (c < 0) - return - m.compare(lo.data(), nb, bits.data(), nb) <= 0 && - m.compare(bits.data(), nb, hi.data(), nb) < 0; - return - m.compare(lo.data(), nb, bits.data(), nb) <= 0 || - m.compare(bits.data(), nb, hi.data(), nb) < 0; + return + m.compare(lo.data(), nw, bits.data(), nw) <= 0 && + m.compare(bits.data(), nw, hi.data(), nw) < 0; + // hi < lo: bits < hi or lo <= bits + return + m.compare(lo.data(), nw, bits.data(), nw) <= 0 || + m.compare(bits.data(), nw, hi.data(), nw) < 0; } bool sls_valuation::eq(svector const& other) const { @@ -65,11 +66,34 @@ namespace bv { return true; } + bool sls_valuation::gt(svector const& a, svector const& b) const { + mpn_manager m; + return m.compare(a.data(), nw, b.data(), nw) > 0; + } + void sls_valuation::clear_overflow_bits(svector& bits) const { for (unsigned i = bw; i < nw * sizeof(digit_t) * 8; ++i) set(bits, i, false); } + bool sls_valuation::get_below(svector const& src, svector& dst) { + for (unsigned i = 0; i < nw; ++i) + dst[i] = (src[i] & ~fixed[i]) | (fixed[i] & bits[i]); + for (unsigned i = 0; i < nw; ++i) + dst[i] = fixed[i] & bits[i]; + if (gt(dst, src)) + return false; + if (!in_range(dst)) { + // lo < hi: + // set dst to lo, except for fixed bits + // + if (gt(hi, lo)) { + + } + } + return true; + } + void sls_valuation::set_value(svector& bits, rational const& n) { for (unsigned i = 0; i < bw; ++i) set(bits, i, n.get_bit(i)); @@ -94,11 +118,16 @@ namespace bv { set(bits, i, true); } - bool sls_valuation::can_set(svector const& new_bits) const { + // + // new_bits != bits => ~fixed + // 0 = (new_bits ^ bits) & fixed + // also check that new_bits are in range + // + bool sls_valuation::can_set(svector const& new_bits) const { for (unsigned i = 0; i < nw; ++i) - if (bits[i] != ((new_bits[i] & ~fixed[i]) | (bits[i] & fixed[i]))) - return true; - return false; + if (0 != ((new_bits[i] ^ bits[i]) & fixed[i])) + return false; + return in_range(new_bits); } unsigned sls_valuation::to_nat(svector const& d, unsigned max_n) { @@ -124,10 +153,15 @@ namespace bv { h = mod(h, rational::power_of_two(bw)); if (h == l) return; - set_value(this->lo, l); - set_value(this->hi, h); + if (eq(lo, hi)) { + set_value(lo, l); + set_value(hi, h); + return; + } + // TODO: intersect with previous range, if any - + set_value(lo, l); + set_value(hi, h); } } diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index 60139f53e49..34ab55f611f 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -28,11 +28,10 @@ Module Name: namespace bv { struct sls_valuation { - unsigned bw; // bit-width - unsigned nw; // num words - svector lo, hi; // range assignment to bit-vector, as wrap-around interval + unsigned bw; // bit-width + unsigned nw; // num words + svector lo, hi; // range assignment to bit-vector, as wrap-around interval svector bits, fixed; // bit assignment and don't care bit - bool is_feasible() const; // the current bit-evaluation is between lo and hi. sls_valuation(unsigned bw); ~sls_valuation(); @@ -44,17 +43,15 @@ namespace bv { void add_range(rational lo, rational hi); void set1(svector& bits); - void clear_overflow_bits(svector& bits) const; + bool in_range(svector const& bits) const; bool can_set(svector const& bits) const; bool eq(sls_valuation const& other) const { return eq(other.bits); } - bool eq(svector const& other) const; - - bool gt(svector const& a, svector const& b) const { - return 0 > memcmp(a.data(), b.data(), num_bytes()); - } + bool eq(svector const& other) const { return eq(other, bits); } + bool eq(svector const& a, svector const& b) const; + bool gt(svector const& a, svector const& b) const; bool is_zero() const { return is_zero(bits); } bool is_zero(svector const& a) const { @@ -79,6 +76,10 @@ namespace bv { return i; } + // retrieve number at or below src which is feasible + // with respect to fixed, lo, hi. + bool get_below(svector const& src, svector& dst); + bool try_set(svector const& src) { if (!can_set(src)) return false; diff --git a/src/test/sls_test.cpp b/src/test/sls_test.cpp index 197fa96c9a6..8e9cc10ad6a 100644 --- a/src/test/sls_test.cpp +++ b/src/test/sls_test.cpp @@ -15,6 +15,12 @@ namespace bv { bv(m) {} + void check_eval(expr* a, expr* b, unsigned j) { + auto es = create_exprs(a, b, j); + for (expr* e : es) + check_eval(e); + } + void check_eval(expr* e) { std::function value = [](expr*, unsigned) { return false; @@ -44,7 +50,7 @@ namespace bv { } else if (m.is_bool(e)) { auto val1 = ev.bval0(e); - auto val2 = m.is_true(r) ? true : false; + auto val2 = m.is_true(r); if (val1 != val2) { verbose_stream() << mk_pp(e, m) << " computed value " << val1 << " at odds with definition\n"; } @@ -53,121 +59,109 @@ namespace bv { } } - void check(expr* a, expr* b) { - expr_ref e(m); - auto& validator = *this; - e = bv.mk_bv_add(a, b); - validator.check_eval(e); - - e = bv.mk_bv_mul(a, b); - validator.check_eval(e); - - e = bv.mk_bv_sub(a, b); - validator.check_eval(e); - - e = bv.mk_bv_udiv(a, b); - validator.check_eval(e); - - e = bv.mk_bv_sdiv(a, b); - validator.check_eval(e); - - e = bv.mk_bv_srem(a, b); - validator.check_eval(e); - - e = bv.mk_bv_urem(a, b); - validator.check_eval(e); - - e = bv.mk_bv_smod(a, b); - validator.check_eval(e); - - e = bv.mk_bv_shl(a, b); - validator.check_eval(e); - - e = bv.mk_bv_ashr(a, b); - validator.check_eval(e); - - e = bv.mk_bv_lshr(a, b); - validator.check_eval(e); - - e = bv.mk_bv_and(a, b); - validator.check_eval(e); - - e = bv.mk_bv_or(a, b); - validator.check_eval(e); - - e = bv.mk_bv_xor(a, b); - validator.check_eval(e); - - e = bv.mk_bv_neg(a); - validator.check_eval(e); - - e = bv.mk_bv_not(a); - validator.check_eval(e); - - e = bv.mk_bvumul_ovfl(a, b); - validator.check_eval(e); - - e = bv.mk_bvumul_no_ovfl(a, b); - validator.check_eval(e); - - e = bv.mk_zero_extend(3, a); - validator.check_eval(e); - - e = bv.mk_sign_extend(3, a); - validator.check_eval(e); - - e = bv.mk_ule(a, b); - validator.check_eval(e); - - e = bv.mk_sle(a, b); - validator.check_eval(e); - - e = bv.mk_concat(a, b); - validator.check_eval(e); - - e = bv.mk_extract(6, 3, a); - validator.check_eval(e); - - e = bv.mk_bvuadd_ovfl(a, b); - validator.check_eval(e); - - -#if 0 - - e = bv.mk_bvsadd_ovfl(a, b); - validator.check_eval(e); - - e = bv.mk_bvneg_ovfl(a); - validator.check_eval(e); - - e = bv.mk_bvsmul_no_ovfl(a, b); - validator.check_eval(e); - - e = bv.mk_bvsmul_no_udfl(a, b); - validator.check_eval(e); - - e = bv.mk_bvsmul_ovfl(a, b); - validator.check_eval(e); - - e = bv.mk_bvsdiv_ovfl(a, b); - validator.check_eval(e); + expr_ref_vector create_exprs(expr* a, expr* b, unsigned j) { + expr_ref_vector result(m); + result.push_back(bv.mk_bv_add(a, b)) + .push_back(bv.mk_bv_mul(a, b)) + .push_back(bv.mk_bv_sub(a, b)) + .push_back(bv.mk_bv_udiv(a, b)) + .push_back(bv.mk_bv_sdiv(a, b)) + .push_back(bv.mk_bv_srem(a, b)) + .push_back(bv.mk_bv_urem(a, b)) + .push_back(bv.mk_bv_smod(a, b)) + .push_back(bv.mk_bv_shl(a, b)) + .push_back(bv.mk_bv_ashr(a, b)) + .push_back(bv.mk_bv_lshr(a, b)) + .push_back(bv.mk_bv_and(a, b)) + .push_back(bv.mk_bv_or(a, b)) + .push_back(bv.mk_bv_xor(a, b)) + .push_back(bv.mk_bv_neg(a)) + .push_back(bv.mk_bv_not(a)) + .push_back(bv.mk_bvumul_ovfl(a, b)) + .push_back(bv.mk_bvumul_no_ovfl(a, b)) + .push_back(bv.mk_zero_extend(3, a)) + .push_back(bv.mk_sign_extend(3, a)) + .push_back(bv.mk_ule(a, b)) + .push_back(bv.mk_sle(a, b)) + .push_back(bv.mk_concat(a, b)) + .push_back(bv.mk_extract(6, 3, a)) + .push_back(bv.mk_bvuadd_ovfl(a, b)) + .push_back(bv.mk_bv_rotate_left(a, j)) + .push_back(bv.mk_bv_rotate_right(a, j)) + .push_back(bv.mk_bv_rotate_left(a, b)) + .push_back(bv.mk_bv_rotate_right(a, b)) + // .push_back(bv.mk_bvsadd_ovfl(a, b)) + // .push_back(bv.mk_bvneg_ovfl(a)) + // .push_back(bv.mk_bvsmul_no_ovfl(a, b)) + // .push_back(bv.mk_bvsmul_no_udfl(a, b)) + // .push_back(bv.mk_bvsmul_ovfl(a, b)) + // .push_back(bv.mk_bvsdiv_ovfl(a, b)) + ; + } -#endif -#if 0 - e = bv.mk_rotate_left(a, b); - validator.check_eval(e); + // e = op(a, b), + // update value of a to "random" + // repair a based on computed values. + void check_repair(expr* a, expr* b, unsigned j) { + expr_ref x(m.mk_const("x", bv.mk_sort(bv.get_bv_size(a))), m); + expr_ref y(m.mk_const("y", bv.mk_sort(bv.get_bv_size(b))), m); + auto es1 = create_exprs(a, b, j); + auto es2 = create_exprs(x, b, j); + auto es3 = create_exprs(a, y, j); + for (unsigned i = 0; i < es1.size(); ++i) { + auto e1 = es1.get(i); + auto e2 = es2.get(i); + auto e3 = es3.get(i); + check_repair_idx(e1, e2, 0, x); + if (is_app(e1) && to_app(e1)->get_num_args() == 2) + check_repair_idx(e1, e3, 1, y); + } + } - e = bv.mk_rotate_right(a, b); - validator.check_eval(e); + random_gen rand; - e = bv.mk_rotate_left_ext(a, b); - validator.check_eval(e); + void check_repair_idx(expr* e1, expr* e2, unsigned idx, expr* x) { + std::function value = [&](expr*, unsigned) { + return rand() % 2 == 0; + }; + expr_ref_vector es(m); + bv_util bv(m); + es.push_back(e1); + es.push_back(e2); + sls_eval ev(m); + ev.init_eval(es, value); + th_rewriter rw(m); + expr_ref r(e1, m); + if (m.is_bool(e1)) { + auto val = m.is_true(r); + auto val2 = ev.bval0(e2); + if (val != val2) { + ev.set(e2, val); + auto rep1 = ev.try_repair(to_app(e2), idx); + if (!rep1) { + verbose_stream() << "Not repaired " << mk_pp(e2, m) << "\n"; + } + SASSERT(rep1); + } + } + if (bv.is_bv(e1)) { + auto& val1 = ev.wval0(e1); + auto& val2 = ev.wval0(e2); + if (!val1.eq(val2)) { + val2.set(val1.bits); + auto rep2 = ev.try_repair(to_app(e2), idx); + if (!rep2) { + verbose_stream() << "Not repaired " << mk_pp(e2, m) << "\n"; + } + SASSERT(rep2); + } + } + } - e = bv.mk_rotate_right_ext(a, b); - validator.check_eval(e); + // todo: + void test_fixed() { -#endif } }; } @@ -183,17 +177,36 @@ static void test_eval1() { bv::sls_test validator(m); unsigned k = 0; - for (unsigned i = 0; i < 256; ++i) { - expr_ref a(bv.mk_numeral(rational(i), 8), m); - for (unsigned j = 0; j < 256; ++j) { - expr_ref b(bv.mk_numeral(rational(j), 8), m); - + unsigned bw = 6; + for (unsigned i = 0; i < 1ul << bw; ++i) { + expr_ref a(bv.mk_numeral(rational(i), bw), m); + for (unsigned j = 0; j < 1ul << bw; ++j) { + expr_ref b(bv.mk_numeral(rational(j), bw), m); ++k; if (k % 1000 == 0) verbose_stream() << "tests " << k << "\n"; + validator.check_eval(a, b, j); + } + } +} - validator.check(a, b); +static void test_repair1() { + ast_manager m; + reg_decl_plugins(m); + bv_util bv(m); + expr_ref e(m); + bv::sls_test validator(m); + unsigned k = 0; + unsigned bw = 6; + for (unsigned i = 0; i < 1ul << bw; ++i) { + expr_ref a(bv.mk_numeral(rational(i), bw), m); + for (unsigned j = 0; j < 1ul << bw; ++j) { + expr_ref b(bv.mk_numeral(rational(j), bw), m); + ++k; + if (k % 1000 == 0) + verbose_stream() << "tests " << k << "\n"; + validator.check_repair(a, b, j); } } }