mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

use default in model construction

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-25 11:16:34 -07:00
parent 39ba9ae501
commit 3205f0d406
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/array_model.cpp
View file

@ -66,7 +66,6 @@ namespace array {
if (!fi->get_else()) { if (!fi->get_else()) {
expr* else_value = nullptr; expr* else_value = nullptr;
unsigned max_occ_num = 0; unsigned max_occ_num = 0;
obj_map<expr, unsigned> num_occ; obj_map<expr, unsigned> num_occ;
for (euf::enode* p : euf::enode_parents(n)) { for (euf::enode* p : euf::enode_parents(n)) {
@ -84,7 +83,6 @@ namespace array {
} }
} }
} }
if (else_value) if (else_value)
fi->set_else(else_value); fi->set_else(else_value);
} }

8
src/sat/smt/bv_delay_internalize.cpp
View file

@ -77,6 +77,7 @@ namespace bv {
if (!check_mul_one(e, args, r1, r2)) if (!check_mul_one(e, args, r1, r2))
return false; return false;
// Add propagation axiom for arguments // Add propagation axiom for arguments
if (!check_mul_invertibility(e, args, r1)) if (!check_mul_invertibility(e, args, r1))
return false; return false;
@ -157,6 +158,7 @@ namespace bv {
return ok; return ok;
} }
/* /*
* Check that multiplication with 0 is correctly propagated. * Check that multiplication with 0 is correctly propagated.
* If not, create algebraic axioms enforcing 0*x = 0 and x*0 = 0 * If not, create algebraic axioms enforcing 0*x = 0 and x*0 = 0
@ -423,9 +425,9 @@ namespace bv {
internalize_mode mode; internalize_mode mode;
switch (to_app(e)->get_decl_kind()) { switch (to_app(e)->get_decl_kind()) {
case OP_BMUL: case OP_BMUL:
case OP_BSMUL_NO_OVFL: //case OP_BSMUL_NO_OVFL:
case OP_BSMUL_NO_UDFL: //case OP_BSMUL_NO_UDFL:
case OP_BUMUL_NO_OVFL: //case OP_BUMUL_NO_OVFL:
case OP_BSMOD_I: case OP_BSMOD_I:
case OP_BUREM_I: case OP_BUREM_I:
case OP_BSREM_I: case OP_BSREM_I: