mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 07:43:41 +00:00
Code Activity

#5211

Browse source 
```
 (declare-fun v5 () Bool)
 (declare-fun i1 () Int)
 (declare-fun i2 () Int)
 (declare-fun i4 () Int)
 (declare-fun i5 () Int)
 (declare-fun i6 () Int)
 (declare-fun i9 () Int)
 (declare-fun i10 () Int)
 (assert (or (not (=> (= 23 i6 i4 i2 85) v5)) (<= i1 8 i9 i9 (+ (+ i1 349 i10 i6) i5)) (>= i4 782)))
 (check-sat)
```
This commit is contained in:
Nikolaj Bjorner 2021-04-22 22:10:39 -07:00
parent bcb33a5b3a
commit 5cfe273460
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -164,7 +164,7 @@ namespace arith {
unsigned index = 0; unsigned index = 0;
while (index < terms.size()) { while (index < terms.size()) {
SASSERT(index >= vars.size()); SASSERT(index >= vars.size());
expr* n = terms[index].get(); expr* n = terms.get(index);
st.to_ensure_enode().push_back(n); st.to_ensure_enode().push_back(n);
if (a.is_add(n)) { if (a.is_add(n)) {
for (expr* arg : *to_app(n)) { for (expr* arg : *to_app(n)) {
@ -391,7 +391,7 @@ namespace arith {
bool solver::internalize_term(expr* term) { bool solver::internalize_term(expr* term) {
if (!has_var(term)) if (!has_var(term))
internalize_def(term); register_theory_var_in_lar_solver(internalize_def(term));
return true; return true;
} }