mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

#5528

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-01 20:39:54 -07:00
parent cf9e55fa96
commit a74c01c8b9
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/arith_internalize.cpp
View file

@ -42,6 +42,7 @@ namespace arith {
void solver::init_internalize() {
force_push();
// initialize 0, 1 variables:
if (!m_internalize_initialized) {
get_one(true);
get_one(false);
@ -484,10 +485,10 @@ namespace arith {
return st.vars()[0];
}
else if (is_one(st) && a.is_numeral(term)) {
return get_one(a.is_int(term));
return lp().local_to_external(get_one(a.is_int(term)));
}
else if (is_zero(st) && a.is_numeral(term)) {
return get_zero(a.is_int(term));
return lp().local_to_external(get_zero(a.is_int(term)));
}
else {
init_left_side(st);