mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix build of unit test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-07-15 19:39:59 -07:00
parent c7f67f9a72
commit 5767dfac49
5 changed files with 11 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/sls/bv_sls_eval.cpp
View file

@ -634,6 +634,10 @@ namespace bv {
bool sls_eval::repair_down(app* e, unsigned i) {
if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) {
ctx.new_value_eh(e->get_arg(i));
if (eval_is_correct(e))
commit_eval(e);
else
ctx.new_value_eh(e); // re-queue repair
return true;
}
return false;

4
src/ast/sls/bv_sls_eval.h
View file

@ -133,6 +133,8 @@ namespace bv {
bool can_eval1(app* e) const;
void commit_eval(app* e);
public:
sls_eval(sls_terms& terms, sls::context& ctx);
@ -154,8 +156,6 @@ namespace bv {
sls_valuation& eval(app* e) const;
void commit_eval(app* e);
void set_random(app* e);
bool eval_is_correct(app* e);

2
src/ast/sls/sls_basic_plugin.cpp
View file

@ -267,7 +267,7 @@ namespace sls {
if (try_repair(e, j))
return;
}
set_value(e, bval1(e));
repair_up(e);
}
bool basic_plugin::try_repair_distinct(app* e, unsigned i) {

6
src/ast/sls/sls_bv_plugin.cpp
View file

@ -100,10 +100,8 @@ namespace sls {
void bv_plugin::repair_down(app* e) {
unsigned n = e->get_num_args();
if (n == 0 || m_eval.eval_is_correct(e)) {
m_eval.commit_eval(e);
return;
}
if (n == 0 || m_eval.eval_is_correct(e))
return;
if (n == 2) {
auto d1 = get_depth(e->get_arg(0));

4
src/test/sls_test.cpp
View file

@ -178,7 +178,7 @@ namespace bv {
auto val2 = ev.bval0(e2);
if (val != val2) {
ev.set(e2, val);
auto rep1 = ev.try_repair(to_app(e2), idx);
auto rep1 = ev.repair_down(to_app(e2), idx);
if (!rep1) {
verbose_stream() << "Not repaired " << mk_pp(e1, m) << " " << mk_pp(e2, m) << " r: " << r << "\n";
}
@ -196,7 +196,7 @@ namespace bv {
auto& val2 = ev.wval(e2);
if (!val1.eq(val2)) {
val2.set(val1.bits());
auto rep2 = ev.try_repair(to_app(e2), idx);
auto rep2 = ev.repair_down(to_app(e2), idx);
if (!rep2) {
verbose_stream() << "Not repaired " << mk_pp(e2, m) << "\n";
}