From fd5902f76eb312d81bcd12ef7fd140a80e31670a Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 16 Jul 2023 11:55:42 -1000 Subject: [PATCH] relax an assertion in int_solver::patcher --- src/math/lp/int_solver.cpp | 13 +- src/math/lp/lar_solver.cpp | 2 +- src/math/lp/lar_solver.h | 1 + z3.log | 1206 ++++++++++++++++++++++++++++++++++++ 4 files changed, 1215 insertions(+), 7 deletions(-) create mode 100644 z3.log diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index fc1c8d3dc..34666e040 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -150,21 +150,22 @@ namespace lp { } for (auto const& c : A.column(j)) { unsigned row_index = c.var(); - unsigned i = lrac.m_r_basis[row_index]; - auto old_val = lia.get_value(i); + unsigned bj = lrac.m_r_basis[row_index]; + auto old_val = lia.get_value(bj); auto new_val = old_val - impq(c.coeff()*delta); - if (lia.has_lower(i) && new_val < lra.get_lower_bound(i)) + if (lia.has_lower(bj) && new_val < lra.get_lower_bound(bj)) return false; - if (lia.has_upper(i) && new_val > lra.get_upper_bound(i)) + if (lia.has_upper(bj) && new_val > lra.get_upper_bound(bj)) return false; if (old_val.is_int() && !new_val.is_int()){ return false; // do not waste resources on this case } - lp_assert(i != v || new_val.is_int()) + // if bj == v, then, because we are patching the lra.get_value(v), + // we just need to assert that the lra.get_value(v) would be integral. + lp_assert(bj != v || lra.from_model_in_impq_to_mpq(new_val).is_int()); } lra.set_value_for_nbasic_column(j, lia.get_value(j) + impq(delta)); - return true; } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index f4067d9bb..dd4f10be8 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1019,7 +1019,7 @@ namespace lp { SASSERT(get_status() == lp_status::OPTIMAL || get_status() == lp_status::FEASIBLE); SASSERT(m_columns_with_changed_bounds.empty()); numeric_pair const& rp = get_column_value(j); - return rp.x + m_delta * rp.y; + return from_model_in_impq_to_mpq(rp); } mpq lar_solver::get_tv_value(tv const& t) const { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index e73e6818c..fc58d0a70 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -497,6 +497,7 @@ class lar_solver : public column_namer { std::ostream& display(std::ostream& out) const; bool init_model() const; + mpq from_model_in_impq_to_mpq(const impq& v) const { return v.x + m_delta * v.y; } mpq get_value(column_index const& j) const; mpq get_tv_value(tv const& t) const; const impq& get_tv_ivalue(tv const& t) const; diff --git a/z3.log b/z3.log new file mode 100644 index 000000000..54f98cda4 --- /dev/null +++ b/z3.log @@ -0,0 +1,1206 @@ +[tool-version] Z3 4.12.3 +[mk-app] #1 true +[mk-app] #2 false +[mk-app] #1 true +[mk-app] #2 false +[mk-app] #3 pi +[mk-app] #4 euler +[mk-var] datatype#0 0 +[mk-var] datatype#1 1 +[mk-app] datatype#2 insert datatype#0 datatype#1 +[mk-app] datatype#3 pattern datatype#2 +[mk-app] datatype#4 head datatype#2 +[mk-app] datatype#5 = datatype#0 datatype#4 +[mk-quant] datatype#6 constructor_accessor_axiom 2 datatype#3 datatype#5 +[attach-var-names] datatype#6 (;k!0) (;List) +[mk-app] datatype#7 tail datatype#2 +[mk-app] datatype#8 = datatype#1 datatype#7 +[mk-quant] datatype#9 constructor_accessor_axiom 2 datatype#3 datatype#8 +[attach-var-names] datatype#9 (;k!0) (;List) +[mk-app] #5 bv +[attach-meaning] #5 bv #b1 +[mk-app] #6 bv +[attach-meaning] #6 bv #b0 +[attach-meaning] #5 bv #b1 +[attach-meaning] #6 bv #b0 +[attach-meaning] #6 bv #b0 +[mk-var] #7 0 +[mk-var] #8 1 +[mk-var] #9 2 +[mk-var] #10 3 +[mk-var] #11 4 +[mk-var] #12 5 +[mk-var] #13 6 +[mk-var] #14 7 +[mk-var] #15 8 +[mk-var] #16 9 +[mk-var] #17 10 +[mk-var] #18 11 +[mk-var] #19 12 +[mk-var] #20 13 +[mk-var] #21 14 +[mk-app] #22 + #15 #13 +[attach-enode] #1 0 +[attach-enode] #2 0 +[mk-app] #23 Int +[attach-meaning] #23 arith 0 +[mk-app] #24 d +[mk-app] #25 to_real #23 +[mk-app] #26 = #25 #24 +[mk-app] #27 not #26 +[mk-app] #28 Real +[attach-meaning] #28 arith 0 +[inst-discovered] theory-solving 0000000000000000 arith# ; #25 +[mk-app] #29 = #25 #28 +[instance] 0000000000000000 #29 +[attach-enode] #29 0 +[end-of-instance] +[mk-app] #29 Real +[attach-meaning] #29 arith (- 1) +[mk-app] #30 * #29 #24 +[mk-app] #31 = #24 #28 +[mk-app] #29 = #28 #24 +[inst-discovered] theory-solving 0000000000000000 arith# ; #29 +[mk-app] #30 = #29 #31 +[instance] 0000000000000000 #30 +[attach-enode] #30 0 +[end-of-instance] +[mk-app] #29 not #31 +[mk-app] #30 c +[mk-app] #32 f +[mk-app] #33 = #30 #32 +[mk-app] #34 b +[mk-app] #35 g +[mk-app] #36 to_int #34 +[mk-app] #37 to_int #35 +[mk-app] #38 mod #36 #37 +[mk-app] #39 e +[mk-app] #40 to_real #38 +[mk-app] #41 * #40 #39 +[mk-app] #42 + #41 +[mk-app] #43 * #42 +[mk-app] #44 a +[mk-app] #45 < #43 #28 +[mk-app] #46 < #28 #39 +[mk-app] #47 < #39 #44 +[mk-app] #48 and #45 #46 #47 +[mk-app] #49 <= #28 #34 +[mk-app] #50 <= #34 #35 +[mk-app] #51 and #49 #50 +[mk-app] #52 and #33 #48 #51 +[mk-app] #53 to_int #32 +[mk-app] #54 mod #36 #53 +[mk-app] #55 to_real #54 +[mk-app] #56 + #39 #55 +[mk-app] #57 * #56 +[mk-app] #58 < #25 #57 +[mk-app] #59 < #57 #25 +[mk-app] #60 and #58 #59 +[mk-app] #61 = #52 #60 +[mk-app] #62 not #61 +[mk-app] #63 * #39 #40 +[inst-discovered] theory-solving 0000000000000000 arith# ; #41 +[mk-app] #64 = #41 #63 +[instance] 0000000000000000 #64 +[attach-enode] #64 0 +[end-of-instance] +[mk-app] #64 + #63 +[inst-discovered] theory-solving 0000000000000000 arith# ; #64 +[mk-app] #65 = #64 #63 +[instance] 0000000000000000 #65 +[attach-enode] #65 0 +[end-of-instance] +[mk-app] #64 * #63 +[inst-discovered] theory-solving 0000000000000000 arith# ; #64 +[mk-app] #65 = #64 #63 +[instance] 0000000000000000 #65 +[attach-enode] #65 0 +[end-of-instance] +[mk-app] #64 <= #28 #63 +[mk-app] #65 not #64 +[mk-app] #66 < #63 #28 +[inst-discovered] theory-solving 0000000000000000 arith# ; #66 +[mk-app] #67 = #66 #65 +[instance] 0000000000000000 #67 +[attach-enode] #67 0 +[end-of-instance] +[mk-app] #66 Real +[attach-meaning] #66 arith (- 1) +[mk-app] #67 * #66 #63 +[mk-app] #68 >= #63 #28 +[inst-discovered] theory-solving 0000000000000000 arith# ; #64 +[mk-app] #66 = #64 #68 +[instance] 0000000000000000 #66 +[attach-enode] #66 0 +[end-of-instance] +[mk-app] #66 not #68 +[mk-app] #67 <= #39 #28 +[mk-app] #69 not #67 +[inst-discovered] theory-solving 0000000000000000 arith# ; #46 +[mk-app] #70 = #46 #69 +[instance] 0000000000000000 #70 +[attach-enode] #70 0 +[end-of-instance] +[mk-app] #70 <= #44 #39 +[mk-app] #71 not #70 +[inst-discovered] theory-solving 0000000000000000 arith# ; #47 +[mk-app] #72 = #47 #71 +[instance] 0000000000000000 #72 +[attach-enode] #72 0 +[end-of-instance] +[mk-app] #72 Real +[attach-meaning] #72 arith (- 1) +[mk-app] #73 * #72 #39 +[mk-app] #74 + #73 #44 +[attach-meaning] #72 arith (- 1) +[mk-app] #75 * #72 #44 +[mk-app] #76 + #39 #75 +[mk-app] #73 >= #76 #28 +[inst-discovered] theory-solving 0000000000000000 arith# ; #70 +[mk-app] #74 = #70 #73 +[instance] 0000000000000000 #74 +[attach-enode] #74 0 +[end-of-instance] +[mk-app] #74 not #73 +[attach-meaning] #72 arith (- 1) +[mk-app] #77 * #72 #34 +[mk-app] #78 >= #34 #28 +[inst-discovered] theory-solving 0000000000000000 arith# ; #49 +[mk-app] #77 = #49 #78 +[instance] 0000000000000000 #77 +[attach-enode] #77 0 +[end-of-instance] +[attach-meaning] #72 arith (- 1) +[mk-app] #77 * #72 #35 +[mk-app] #79 + #34 #77 +[mk-app] #80 <= #79 #28 +[inst-discovered] theory-solving 0000000000000000 arith# ; #50 +[mk-app] #81 = #50 #80 +[instance] 0000000000000000 #81 +[attach-enode] #81 0 +[end-of-instance] +[mk-app] #81 and #33 #66 #69 #74 #78 #80 +[inst-discovered] theory-solving 0000000000000000 arith# ; #25 +[mk-app] #82 = #25 #28 +[instance] 0000000000000000 #82 +[attach-enode] #82 0 +[end-of-instance] +[inst-discovered] theory-solving 0000000000000000 arith# ; #57 +[mk-app] #82 = #57 #56 +[instance] 0000000000000000 #82 +[attach-enode] #82 0 +[end-of-instance] +[mk-app] #82 <= #56 #28 +[mk-app] #83 not #82 +[mk-app] #84 < #28 #56 +[inst-discovered] theory-solving 0000000000000000 arith# ; #84 +[mk-app] #85 = #84 #83 +[instance] 0000000000000000 #85 +[attach-enode] #85 0 +[end-of-instance] +[mk-app] #84 <= #28 #56 +[mk-app] #85 not #84 +[mk-app] #86 < #56 #28 +[inst-discovered] theory-solving 0000000000000000 arith# ; #86 +[mk-app] #87 = #86 #85 +[instance] 0000000000000000 #87 +[attach-enode] #87 0 +[end-of-instance] +[attach-meaning] #72 arith (- 1) +[mk-app] #86 * #72 #39 +[attach-meaning] #72 arith (- 1) +[mk-app] #87 * #72 #55 +[mk-app] #88 + #86 #87 +[mk-app] #86 >= #56 #28 +[inst-discovered] theory-solving 0000000000000000 arith# ; #84 +[mk-app] #87 = #84 #86 +[instance] 0000000000000000 #87 +[attach-enode] #87 0 +[end-of-instance] +[mk-app] #87 not #86 +[mk-app] #88 and #83 #87 +[mk-app] #89 = #81 #88 +[mk-app] #90 not #81 +[mk-app] #91 not #89 +[inst-discovered] theory-solving 0000000000000000 basic# ; #91 +[mk-app] #90 = #91 #91 +[instance] 0000000000000000 #90 +[attach-enode] #90 0 +[end-of-instance] +[attach-meaning] #5 bv #b1 +[attach-meaning] #6 bv #b0 +[attach-meaning] #5 bv #b1 +[attach-meaning] #6 bv #b0 +[inst-discovered] theory-solving 0000000000000000 arith# ; #25 +[mk-app] #90 = #25 #28 +[instance] 0000000000000000 #90 +[attach-enode] #90 0 +[end-of-instance] +[mk-app] #90 = #28 #24 +[mk-app] #92 not #90 +[inst-discovered] theory-solving 0000000000000000 arith# ; #41 +[mk-app] #93 = #41 #63 +[instance] 0000000000000000 #93 +[attach-enode] #93 0 +[end-of-instance] +[mk-app] #93 + #63 +[inst-discovered] theory-solving 0000000000000000 arith# ; #93 +[mk-app] #94 = #93 #63 +[instance] 0000000000000000 #94 +[attach-enode] #94 0 +[end-of-instance] +[mk-app] #93 * #63 +[inst-discovered] theory-solving 0000000000000000 arith# ; #93 +[mk-app] #94 = #93 #63 +[instance] 0000000000000000 #94 +[attach-enode] #94 0 +[end-of-instance] +[mk-app] #93 < #63 #28 +[inst-discovered] theory-solving 0000000000000000 arith# ; #93 +[mk-app] #94 = #93 #65 +[instance] 0000000000000000 #94 +[attach-enode] #94 0 +[end-of-instance] +[inst-discovered] theory-solving 0000000000000000 arith# ; #46 +[mk-app] #93 = #46 #69 +[instance] 0000000000000000 #93 +[attach-enode] #93 0 +[end-of-instance] +[inst-discovered] theory-solving 0000000000000000 arith# ; #47 +[mk-app] #93 = #47 #71 +[instance] 0000000000000000 #93 +[attach-enode] #93 0 +[end-of-instance] +[mk-app] #93 and #33 #65 #69 #71 #49 #50 +[inst-discovered] theory-solving 0000000000000000 arith# ; #57 +[mk-app] #94 = #57 #56 +[instance] 0000000000000000 #94 +[attach-enode] #94 0 +[end-of-instance] +[mk-app] #94 < #28 #56 +[inst-discovered] theory-solving 0000000000000000 arith# ; #94 +[mk-app] #95 = #94 #83 +[instance] 0000000000000000 #95 +[attach-enode] #95 0 +[end-of-instance] +[mk-app] #94 < #56 #28 +[inst-discovered] theory-solving 0000000000000000 arith# ; #94 +[mk-app] #95 = #94 #85 +[instance] 0000000000000000 #95 +[attach-enode] #95 0 +[end-of-instance] +[mk-app] #94 and #83 #85 +[mk-app] #95 = #93 #94 +[mk-app] #96 not #93 +[mk-app] #97 not #95 +[inst-discovered] theory-solving 0000000000000000 basic# ; #97 +[mk-app] #96 = #97 #97 +[instance] 0000000000000000 #96 +[attach-enode] #96 0 +[end-of-instance] +[mk-app] #96 not #93 +[inst-discovered] theory-solving 0000000000000000 basic# ; #97 +[mk-app] #96 = #97 #97 +[instance] 0000000000000000 #96 +[attach-enode] #96 0 +[end-of-instance] +[inst-discovered] theory-solving 0000000000000000 arith# ; #56 +[mk-app] #96 = #56 #56 +[instance] 0000000000000000 #96 +[attach-enode] #96 0 +[end-of-instance] +[mk-app] #96 not #93 +[inst-discovered] theory-solving 0000000000000000 basic# ; #97 +[mk-app] #96 = #97 #97 +[instance] 0000000000000000 #96 +[attach-enode] #96 0 +[end-of-instance] +[mk-app] #96 Real +[attach-meaning] #96 arith 1 +[mk-app] #98 + #28 #96 +[mk-app] #99 k!0 +[mk-app] #100 if #99 #28 #98 +[mk-app] #101 not #99 +[mk-app] #92 + #32 #96 +[mk-app] #102 k!1 +[mk-app] #103 if #102 #32 #92 +[mk-app] #104 k!2 +[mk-app] #105 + #39 #96 +[mk-app] #106 if #104 #39 #105 +[mk-app] #107 not #104 +[mk-app] #108 and #102 #65 #69 #107 #49 #50 +[mk-app] #109 = #108 #94 +[mk-app] #110 not #109 +[mk-app] #93 k!3 +[mk-app] #95 not #93 +[mk-app] #97 k!4 +[mk-app] #111 not #97 +[mk-app] #112 and #102 #65 #69 #97 #49 #50 +[mk-app] #113 = #112 #94 +[mk-app] #114 not #113 +[attach-meaning] #6 bv #b0 +[attach-enode] #1 0 +[attach-enode] #2 0 +[attach-meaning] #72 arith (- 1) +[mk-app] #107 * #72 #63 +[inst-discovered] theory-solving 0000000000000000 arith# ; #64 +[mk-app] #107 = #64 #68 +[instance] 0000000000000000 #107 +[attach-enode] #107 0 +[end-of-instance] +[attach-meaning] #72 arith (- 1) +[mk-app] #107 * #72 #34 +[inst-discovered] theory-solving 0000000000000000 arith# ; #49 +[mk-app] #107 = #49 #78 +[instance] 0000000000000000 #107 +[attach-enode] #107 0 +[end-of-instance] +[attach-meaning] #72 arith (- 1) +[inst-discovered] theory-solving 0000000000000000 arith# ; #50 +[mk-app] #107 = #50 #80 +[instance] 0000000000000000 #107 +[attach-enode] #107 0 +[end-of-instance] +[mk-app] #107 and #102 #66 #69 #97 #78 #80 +[attach-meaning] #72 arith (- 1) +[mk-app] #101 * #72 #39 +[attach-meaning] #72 arith (- 1) +[mk-app] #90 * #72 #55 +[mk-app] #108 + #101 #90 +[inst-discovered] theory-solving 0000000000000000 arith# ; #84 +[mk-app] #101 = #84 #86 +[instance] 0000000000000000 #101 +[attach-enode] #101 0 +[end-of-instance] +[mk-app] #101 = #107 #88 +[mk-app] #90 not #107 +[mk-app] #108 not #101 +[inst-discovered] theory-solving 0000000000000000 basic# ; #108 +[mk-app] #90 = #108 #108 +[instance] 0000000000000000 #90 +[attach-enode] #90 0 +[end-of-instance] +[begin-check] 0 +[mk-app] #90 Int +[attach-meaning] #90 arith 1 +[attach-enode] #90 0 +[attach-enode] #96 0 +[attach-enode] #23 0 +[attach-enode] #28 0 +[mk-app] #109 not #107 +[inst-discovered] theory-solving 0000000000000000 basic# ; #108 +[mk-app] #109 = #108 #108 +[instance] 0000000000000000 #109 +[attach-enode] #109 0 +[end-of-instance] +[mk-app] #109 not #107 +[inst-discovered] theory-solving 0000000000000000 basic# ; #108 +[mk-app] #109 = #108 #108 +[instance] 0000000000000000 #109 +[attach-enode] #109 0 +[end-of-instance] +[mk-app] #109 not #107 +[inst-discovered] theory-solving 0000000000000000 basic# ; #108 +[mk-app] #109 = #108 #108 +[instance] 0000000000000000 #109 +[attach-enode] #109 0 +[end-of-instance] +[mk-app] #109 not #102 +[mk-app] #110 not #78 +[mk-app] #115 not #80 +[mk-app] #116 or #67 #68 #109 #110 #111 #115 +[mk-app] #117 not #116 +[inst-discovered] theory-solving 0000000000000000 basic# ; #107 +[mk-app] #118 = #107 #117 +[instance] 0000000000000000 #118 +[attach-enode] #118 0 +[end-of-instance] +[mk-app] #118 or #82 #86 +[mk-app] #119 not #118 +[inst-discovered] theory-solving 0000000000000000 basic# ; #88 +[mk-app] #120 = #88 #119 +[instance] 0000000000000000 #120 +[attach-enode] #120 0 +[end-of-instance] +[mk-app] #120 = #116 #118 +[mk-app] #121 = #117 #119 +[inst-discovered] theory-solving 0000000000000000 basic# ; #121 +[mk-app] #122 = #121 #120 +[instance] 0000000000000000 #122 +[attach-enode] #122 0 +[end-of-instance] +[mk-app] #117 not #116 +[mk-app] #121 not #120 +[inst-discovered] theory-solving 0000000000000000 basic# ; #121 +[mk-app] #117 = #121 #121 +[instance] 0000000000000000 #117 +[attach-enode] #117 0 +[end-of-instance] +[mk-app] #107 not #116 +[inst-discovered] theory-solving 0000000000000000 basic# ; #121 +[mk-app] #107 = #121 #121 +[instance] 0000000000000000 #107 +[attach-enode] #107 0 +[end-of-instance] +[mk-app] #107 not #116 +[inst-discovered] theory-solving 0000000000000000 basic# ; #121 +[mk-app] #107 = #121 #121 +[instance] 0000000000000000 #107 +[attach-enode] #107 0 +[end-of-instance] +[assign] #93 justification -1: +[attach-enode] #39 0 +[attach-enode] #34 0 +[attach-enode] #36 0 +[attach-enode] #35 0 +[attach-enode] #37 0 +[attach-enode] #38 0 +[mk-app] #119 mod #36 #23 +[mk-app] #107 mod0 #36 #23 +[mk-app] #101 = #107 #119 +[attach-enode] #107 0 +[attach-enode] #119 0 +[attach-enode] #101 0 +[mk-app] #108 Int +[attach-meaning] #108 arith (- 1) +[mk-app] #117 * #108 #119 +[mk-app] #122 + #107 #117 +[mk-app] #123 <= #122 #23 +[mk-app] #124 >= #122 #23 +[attach-enode] #108 0 +[attach-enode] #117 0 +[attach-enode] #122 0 +[mk-app] #125 to_real #36 +[mk-app] #126 - #125 #34 +[mk-app] #127 <= #126 #28 +[mk-app] #128 - #34 #125 +[mk-app] #129 >= #128 #96 +[attach-enode] #125 0 +[attach-enode] #126 0 +[attach-enode] #127 0 +[attach-enode] #128 0 +[attach-enode] #129 0 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #127 +[assign] #127 justification -1: 0 +[end-of-instance] +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #129 +[assign] (not #129) justification -1: 0 +[end-of-instance] +[assign] #101 axiom +[attach-enode] #40 0 +[attach-enode] #63 0 +[attach-enode] #72 0 +[attach-enode] #77 0 +[attach-enode] #79 0 +[attach-enode] #32 0 +[attach-enode] #53 0 +[attach-enode] #54 0 +[attach-enode] #55 0 +[attach-enode] #56 0 +[assign] (not #120) justification -1: +[assign] #124 bin 4 +[assign] #123 bin 4 +[mk-app] #130 = #122 #23 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #130 +[end-of-instance] +[push] 0 +[assign] (not #86) decision axiom +[assign] #82 bin -15 +[assign] #118 bin 14 +[assign] (not #116) clause -13 -16 +[assign] #80 bin -13 +[assign] #97 bin -13 +[assign] #78 bin -13 +[assign] #102 bin -13 +[assign] (not #68) bin -13 +[assign] (not #67) bin -13 +[mk-app] #130 div #36 #53 +[mk-app] #131 * #53 #130 +[mk-app] #132 + #131 #54 +[mk-app] #133 = #36 #132 +[attach-enode] #130 0 +[mk-app] #134 div0 #36 #53 +[mk-app] #135 = #130 #134 +[attach-enode] #134 0 +[attach-enode] #135 0 +[attach-meaning] #108 arith (- 1) +[mk-app] #136 * #108 #134 +[mk-app] #137 + #130 #136 +[mk-app] #138 <= #137 #23 +[mk-app] #139 >= #137 #23 +[attach-enode] #136 0 +[attach-enode] #137 0 +[assign] #135 axiom +[attach-enode] #131 0 +[attach-enode] #132 0 +[attach-enode] #133 0 +[attach-meaning] #108 arith (- 1) +[mk-app] #140 * #108 #132 +[mk-app] #141 + #36 #140 +[mk-app] #142 <= #141 #23 +[mk-app] #143 >= #141 #23 +[attach-enode] #140 0 +[attach-enode] #141 0 +[mk-app] #144 - #53 +[mk-app] #145 >= #53 #23 +[mk-app] #146 if #145 #53 #144 +[attach-meaning] #108 arith (- 1) +[mk-app] #147 - #54 #146 +[mk-app] #148 = #53 #23 +[attach-enode] #148 0 +[mk-app] #149 = #23 #53 +[mk-app] #150 <= #53 #23 +[attach-enode] #149 0 +[mk-app] #151 >= #54 #23 +[attach-enode] #151 0 +[mk-app] #152 <= #147 #108 +[attach-enode] #145 0 +[attach-enode] #144 0 +[mk-app] #153 = #53 #146 +[mk-app] #154 = #144 #146 +[attach-enode] #146 0 +[attach-enode] #153 0 +[attach-enode] #154 0 +[attach-enode] #147 0 +[attach-enode] #152 0 +[mk-app] #155 - #36 #131 +[mk-app] #156 >= #155 #23 +[attach-meaning] #108 arith (- 1) +[mk-app] #157 * #108 #131 +[mk-app] #158 + #36 #157 +[inst-discovered] theory-solving 0000000000000000 arith# ; #155 +[mk-app] #159 = #155 #158 +[instance] 0000000000000000 #159 +[attach-enode] #159 0 +[end-of-instance] +[mk-app] #159 >= #158 #23 +[attach-enode] #157 0 +[attach-enode] #158 0 +[attach-enode] #159 0 +[mk-app] #155 div #36 #37 +[mk-app] #156 * #37 #155 +[mk-app] #160 + #156 #38 +[mk-app] #161 = #36 #160 +[attach-enode] #155 0 +[mk-app] #162 div0 #36 #37 +[mk-app] #163 = #155 #162 +[attach-enode] #162 0 +[attach-enode] #163 0 +[attach-meaning] #108 arith (- 1) +[mk-app] #164 * #108 #162 +[mk-app] #165 + #155 #164 +[mk-app] #166 <= #165 #23 +[mk-app] #167 >= #165 #23 +[attach-enode] #164 0 +[attach-enode] #165 0 +[assign] #163 axiom +[attach-enode] #156 0 +[attach-enode] #160 0 +[attach-enode] #161 0 +[attach-meaning] #108 arith (- 1) +[mk-app] #168 * #108 #160 +[mk-app] #169 + #36 #168 +[mk-app] #170 <= #169 #23 +[mk-app] #171 >= #169 #23 +[attach-enode] #168 0 +[attach-enode] #169 0 +[mk-app] #172 - #37 +[mk-app] #173 >= #37 #23 +[mk-app] #174 if #173 #37 #172 +[attach-meaning] #108 arith (- 1) +[mk-app] #175 - #38 #174 +[mk-app] #176 = #37 #23 +[attach-enode] #176 0 +[mk-app] #177 = #23 #37 +[mk-app] #178 <= #37 #23 +[attach-enode] #177 0 +[mk-app] #179 >= #38 #23 +[attach-enode] #179 0 +[mk-app] #180 <= #175 #108 +[attach-enode] #173 0 +[attach-enode] #172 0 +[mk-app] #181 = #37 #174 +[mk-app] #182 = #172 #174 +[attach-enode] #174 0 +[attach-enode] #181 0 +[attach-enode] #182 0 +[attach-enode] #175 0 +[attach-enode] #180 0 +[mk-app] #183 - #36 #156 +[mk-app] #184 >= #183 #23 +[attach-meaning] #108 arith (- 1) +[mk-app] #185 * #108 #156 +[mk-app] #186 + #36 #185 +[inst-discovered] theory-solving 0000000000000000 arith# ; #183 +[mk-app] #187 = #183 #186 +[instance] 0000000000000000 #187 +[attach-enode] #187 0 +[end-of-instance] +[mk-app] #187 >= #186 #23 +[attach-enode] #185 0 +[attach-enode] #186 0 +[attach-enode] #187 0 +[mk-app] #183 to_real #53 +[mk-app] #184 - #183 #32 +[mk-app] #188 <= #184 #28 +[mk-app] #189 - #32 #183 +[mk-app] #190 >= #189 #96 +[attach-enode] #183 0 +[attach-enode] #184 0 +[attach-enode] #188 0 +[attach-enode] #189 0 +[attach-enode] #190 0 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #188 +[assign] #188 justification -1: 0 +[end-of-instance] +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #190 +[assign] (not #190) justification -1: 0 +[end-of-instance] +[mk-app] #191 to_real #37 +[mk-app] #192 - #191 #35 +[mk-app] #193 <= #192 #28 +[mk-app] #194 - #35 #191 +[mk-app] #195 >= #194 #96 +[attach-enode] #191 0 +[attach-enode] #192 0 +[attach-enode] #193 0 +[attach-enode] #194 0 +[attach-enode] #195 0 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #193 +[assign] #193 justification -1: 0 +[end-of-instance] +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #195 +[assign] (not #195) justification -1: 0 +[end-of-instance] +[assign] (not #151) clause -28 -14 2 +[assign] #138 clause 19 -18 +[assign] #139 clause 20 -18 +[assign] #166 clause 34 -33 +[assign] #167 clause 35 -33 +[assign] #148 clause 24 28 +[assign] #149 justification -1: 24 +[mk-app] #196 = #54 #119 +[attach-meaning] #108 arith (- 1) +[mk-app] #197 + #54 #117 +[mk-app] #198 <= #197 #23 +[mk-app] #199 >= #197 #23 +[assign] #196 justification -1: 24 +[attach-enode] #196 0 +[attach-enode] #197 0 +[assign] #198 justification -1: 52 +[assign] #199 justification -1: 52 +[mk-app] #200 = #137 #23 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #200 +[end-of-instance] +[mk-app] #200 = #165 #23 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #200 +[end-of-instance] +[assign] #150 clause 26 -25 +[assign] #145 clause 27 -25 +[assign] #153 clause 30 -27 +[mk-app] #200 = #197 #23 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #200 +[end-of-instance] +[mk-app] #200 = #23 #144 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #200 +[end-of-instance] +[mk-app] #200 = #28 #183 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #200 +[end-of-instance] +[mk-app] #200 = #32 #189 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #200 +[end-of-instance] +[assign] #154 justification -1: 30 24 26 27 +[push] 1 +[assign] (not #179) decision axiom +[assign] #176 clause 39 43 +[assign] #177 justification -1: 39 +[mk-app] #200 = #38 #119 +[attach-meaning] #108 arith (- 1) +[mk-app] #201 + #38 #117 +[mk-app] #202 <= #201 #23 +[mk-app] #203 >= #201 #23 +[assign] #200 justification -1: 39 +[attach-enode] #200 0 +[attach-enode] #201 0 +[assign] #202 justification -1: 55 +[assign] #203 justification -1: 55 +[mk-app] #204 = #130 #155 +[attach-meaning] #108 arith (- 1) +[mk-app] #205 * #108 #155 +[mk-app] #206 + #130 #205 +[mk-app] #207 <= #206 #23 +[mk-app] #208 >= #206 #23 +[assign] #204 justification -1: 39 24 +[attach-enode] #204 0 +[attach-enode] #205 0 +[attach-enode] #206 0 +[assign] #207 justification -1: 58 +[assign] #208 justification -1: 58 +[mk-app] #209 = #144 #172 +[attach-meaning] #108 arith (- 1) +[mk-app] #210 * #108 #172 +[mk-app] #211 + #144 #210 +[mk-app] #212 <= #211 #23 +[mk-app] #213 >= #211 #23 +[assign] #209 justification -1: 39 24 +[attach-enode] #209 0 +[attach-enode] #210 0 +[attach-enode] #211 0 +[assign] #212 justification -1: 61 +[assign] #213 justification -1: 61 +[mk-app] #214 = #183 #191 +[attach-meaning] #72 arith (- 1) +[mk-app] #215 * #72 #191 +[mk-app] #216 + #183 #215 +[mk-app] #217 <= #216 #28 +[mk-app] #218 >= #216 #28 +[assign] #214 justification -1: 39 24 +[attach-enode] #214 0 +[attach-enode] #215 0 +[attach-enode] #216 0 +[assign] #217 justification -1: 64 +[assign] #218 justification -1: 64 +[mk-app] #219 = #40 #55 +[attach-meaning] #72 arith (- 1) +[mk-app] #220 * #72 #55 +[mk-app] #221 + #40 #220 +[mk-app] #222 <= #221 #28 +[mk-app] #223 >= #221 #28 +[assign] #219 justification -1: 24 39 +[attach-enode] #219 0 +[attach-enode] #220 0 +[attach-enode] #221 0 +[assign] #222 justification -1: 67 +[assign] #223 justification -1: 67 +[assign] #178 clause 41 -40 +[assign] #173 clause 42 -40 +[assign] #181 clause 45 -42 +[mk-app] #224 = #201 #23 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #224 +[end-of-instance] +[mk-app] #224 = #206 #23 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #224 +[end-of-instance] +[mk-app] #224 = #211 #23 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #224 +[end-of-instance] +[mk-app] #224 = #216 #28 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #224 +[end-of-instance] +[mk-app] #224 = #221 #28 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #224 +[end-of-instance] +[mk-app] #224 = #35 #194 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #224 +[end-of-instance] +[push] 2 +[assign] (not #152) decision axiom +[push] 3 +[assign] (not #143) decision axiom +[assign] #142 clause 22 23 +[assign] (not #133) clause -21 23 +[assign] (not #159) clause -32 23 -14 2 +[push] 4 +[assign] (not #182) decision axiom +[push] 5 +[assign] (not #187) decision axiom +[push] 6 +[assign] (not #171) decision axiom +[assign] #170 clause 37 38 +[assign] (not #161) clause -36 38 +[push] 7 +[assign] (not #180) decision axiom +[mk-app] #224 = #36 #197 +[attach-enode] #224 0 +[attach-meaning] #108 arith (- 1) +[mk-app] #225 * #108 #197 +[mk-app] #226 + #36 #225 +[mk-app] #227 <= #226 #23 +[mk-app] #228 >= #226 #23 +[attach-enode] #225 0 +[attach-enode] #226 0 +[push] 8 +[assign] #224 decision axiom +[assign] #227 clause 71 -70 +[assign] #228 clause 72 -70 +[mk-app] #229 = #125 #183 +[attach-meaning] #72 arith (- 1) +[mk-app] #230 * #72 #183 +[mk-app] #231 + #125 #230 +[mk-app] #232 <= #231 #28 +[mk-app] #233 >= #231 #28 +[assign] #229 justification -1: 70 24 54 53 +[attach-enode] #229 0 +[attach-enode] #230 0 +[attach-enode] #231 0 +[assign] #232 justification -1: 73 +[assign] #233 justification -1: 73 +[mk-app] #234 = #226 #23 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #234 +[end-of-instance] +[mk-app] #234 = #231 #28 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #234 +[end-of-instance] +[mk-app] #234 not #151 +[mk-app] #235 or #151 #234 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #235 +[end-of-instance] +[mk-app] #234 <= #131 #23 +[assign] #234 justification -1: 26 27 +[mk-app] #235 <= #156 #23 +[assign] #235 justification -1: 41 42 +[resolve-process] true +[resolve-lit] 8 #67 +[resolve-lit] 8 (not #82) +[resolve-lit] 0 (not #234) +[resolve-lit] 5 #143 +[resolve-lit] 0 (not #228) +[resolve-lit] 8 (not #199) +[resolve-process] (not #234) +[resolve-lit] 8 (not #150) +[resolve-lit] 8 (not #145) +[conflict] (not #228) (not #82) #143 +[pop] 5 9 +[attach-enode] #225 0 +[attach-enode] #226 0 +[assign] (not #228) clause -70 23 -14 +[resolve-process] true +[resolve-lit] 3 (not #78) +[resolve-lit] 3 (not #198) +[resolve-lit] 0 #228 +[conflict] #228 (not #78) (not #198) +[pop] 3 4 +[attach-enode] #225 0 +[attach-enode] #226 0 +[assign] #228 clause 55 -10 -53 +[assign] #143 clause 23 -55 -14 +[mk-app] #200 = #226 #36 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #200 +[end-of-instance] +[push] 1 +[assign] (not #179) decision axiom +[assign] #176 clause 39 43 +[assign] #177 justification -1: 39 +[mk-app] #200 = #38 #119 +[attach-meaning] #108 arith (- 1) +[mk-app] #201 + #38 #117 +[mk-app] #202 <= #201 #23 +[mk-app] #203 >= #201 #23 +[assign] #200 justification -1: 39 +[attach-enode] #200 0 +[attach-enode] #201 0 +[assign] #202 justification -1: 56 +[assign] #203 justification -1: 56 +[mk-app] #204 = #130 #155 +[attach-meaning] #108 arith (- 1) +[mk-app] #205 * #108 #155 +[mk-app] #206 + #130 #205 +[mk-app] #207 <= #206 #23 +[mk-app] #208 >= #206 #23 +[assign] #204 justification -1: 39 24 +[attach-enode] #204 0 +[attach-enode] #205 0 +[attach-enode] #206 0 +[assign] #207 justification -1: 59 +[assign] #208 justification -1: 59 +[mk-app] #209 = #144 #172 +[attach-meaning] #108 arith (- 1) +[mk-app] #210 * #108 #172 +[mk-app] #211 + #144 #210 +[mk-app] #212 <= #211 #23 +[mk-app] #213 >= #211 #23 +[assign] #209 justification -1: 39 24 +[attach-enode] #209 0 +[attach-enode] #210 0 +[attach-enode] #211 0 +[assign] #212 justification -1: 62 +[assign] #213 justification -1: 62 +[mk-app] #214 = #183 #191 +[attach-meaning] #72 arith (- 1) +[mk-app] #215 * #72 #191 +[mk-app] #216 + #183 #215 +[mk-app] #217 <= #216 #28 +[mk-app] #218 >= #216 #28 +[assign] #214 justification -1: 39 24 +[attach-enode] #214 0 +[attach-enode] #215 0 +[attach-enode] #216 0 +[assign] #217 justification -1: 65 +[assign] #218 justification -1: 65 +[mk-app] #219 = #40 #55 +[attach-meaning] #72 arith (- 1) +[mk-app] #220 * #72 #55 +[mk-app] #221 + #40 #220 +[mk-app] #222 <= #221 #28 +[mk-app] #223 >= #221 #28 +[assign] #219 justification -1: 24 39 +[attach-enode] #219 0 +[attach-enode] #220 0 +[attach-enode] #221 0 +[assign] #222 justification -1: 68 +[assign] #223 justification -1: 68 +[assign] #178 clause 41 -40 +[assign] #173 clause 42 -40 +[assign] #181 clause 45 -42 +[mk-app] #224 = #201 #23 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #224 +[end-of-instance] +[mk-app] #224 = #206 #23 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #224 +[end-of-instance] +[mk-app] #224 = #211 #23 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #224 +[end-of-instance] +[mk-app] #224 = #216 #28 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #224 +[end-of-instance] +[mk-app] #224 = #221 #28 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #224 +[end-of-instance] +[mk-app] #224 = #35 #194 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #224 +[end-of-instance] +[push] 2 +[assign] (not #152) decision axiom +[push] 3 +[assign] (not #142) decision axiom +[assign] (not #133) clause -21 22 +[push] 4 +[assign] (not #182) decision axiom +[push] 5 +[assign] (not #187) decision axiom +[push] 6 +[assign] (not #171) decision axiom +[assign] #170 clause 37 38 +[assign] (not #161) clause -36 38 +[push] 7 +[assign] (not #180) decision axiom +[push] 8 +[assign] (not #159) decision axiom +[mk-app] #224 = #172 #226 +[attach-enode] #224 0 +[attach-meaning] #108 arith (- 1) +[mk-app] #227 * #108 #226 +[mk-app] #229 + #172 #227 +[mk-app] #230 <= #229 #23 +[mk-app] #231 >= #229 #23 +[attach-enode] #227 0 +[attach-enode] #229 0 +[push] 9 +[assign] #224 decision axiom +[assign] #230 clause 72 -71 +[assign] #231 clause 73 -71 +[mk-app] #232 = #125 #183 +[attach-meaning] #72 arith (- 1) +[mk-app] #233 * #72 #183 +[mk-app] #234 + #125 #233 +[mk-app] #235 <= #234 #28 +[mk-app] #236 >= #234 #28 +[assign] #232 justification -1: 71 24 39 24 53 54 26 27 +[attach-enode] #232 0 +[attach-enode] #233 0 +[attach-enode] #234 0 +[assign] #235 justification -1: 74 +[assign] #236 justification -1: 74 +[mk-app] #237 = #229 #23 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #237 +[end-of-instance] +[mk-app] #237 = #234 #28 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #237 +[end-of-instance] +[mk-app] #237 <= #54 #23 +[assign] #237 justification -1: -28 +[mk-app] #238 not #237 +[mk-app] #239 or #237 #238 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #239 +[end-of-instance] +[mk-app] #238 not #151 +[mk-app] #239 or #151 #238 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #239 +[end-of-instance] +[mk-app] #238 <= #156 #23 +[assign] #238 justification -1: 41 42 +[resolve-process] true +[resolve-lit] 0 (not #238) +[resolve-lit] 8 (not #202) +[resolve-lit] 3 #171 +[resolve-lit] 9 (not #199) +[resolve-lit] 9 #151 +[resolve-lit] 0 (not #230) +[resolve-lit] 8 (not #178) +[resolve-process] (not #238) +[resolve-lit] 8 (not #173) +[conflict] (not #230) (not #202) #171 #151 (not #178) (not #173) +[pop] 3 10 +[attach-enode] #227 0 +[attach-enode] #229 0 +[assign] (not #230) clause -71 38 -57 28 -41 -42 +[resolve-process] true +[resolve-lit] 5 (not #173) +[resolve-lit] 6 (not #228) +[resolve-lit] 0 #230 +[conflict] #230 (not #173) (not #228) +[pop] 5 7 +[attach-enode] #227 0 +[attach-enode] #229 0 +[assign] #230 clause 71 -42 -55 +[assign] #171 clause 38 -71 -57 28 -41 -42 +[push] 2 +[assign] (not #152) decision axiom +[push] 3 +[assign] (not #142) decision axiom +[assign] (not #133) clause -21 22 +[push] 4 +[assign] (not #182) decision axiom +[push] 5 +[assign] (not #187) decision axiom +[push] 6 +[assign] (not #180) decision axiom +[push] 7 +[assign] (not #170) decision axiom +[assign] (not #161) clause -36 37 +[push] 8 +[assign] (not #159) decision axiom +[mk-app] #224 = #197 #226 +[attach-enode] #224 0 +[attach-meaning] #108 arith (- 1) +[mk-app] #231 + #197 #227 +[mk-app] #232 <= #231 #23 +[mk-app] #233 >= #231 #23 +[attach-enode] #231 0 +[push] 9 +[assign] #232 decision axiom +[mk-app] #234 = #231 #229 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #234 +[end-of-instance] +[push] 10 +[assign] #224 decision axiom +[assign] #233 clause 74 -72 +[mk-app] #234 = #125 #183 +[attach-meaning] #72 arith (- 1) +[mk-app] #235 * #72 #183 +[mk-app] #236 + #125 #235 +[mk-app] #237 <= #236 #28 +[mk-app] #238 >= #236 #28 +[assign] #234 justification -1: 72 24 53 54 54 53 +[attach-enode] #234 0 +[attach-enode] #235 0 +[attach-enode] #236 0 +[assign] #237 justification -1: 75 +[assign] #238 justification -1: 75 +[mk-app] #239 = #231 #23 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #239 +[end-of-instance] +[mk-app] #239 = #23 #229 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #239 +[end-of-instance] +[mk-app] #239 = #236 #28 +[inst-discovered] theory-solving 0000000000000000 arith# +[instance] 0000000000000000 #239 +[end-of-instance] +[attach-meaning] #108 arith (- 1) +[attach-meaning] #108 arith (- 1) +[attach-meaning] #108 arith (- 1) +[attach-meaning] #72 arith (- 1) +[attach-meaning] #72 arith (- 1) +[attach-meaning] #108 arith (- 1) +[attach-meaning] #72 arith (- 1) +[attach-meaning] #108 arith (- 1) +[attach-meaning] #108 arith (- 1) +[attach-meaning] #108 arith (- 1) +[attach-meaning] #108 arith (- 1) +[attach-meaning] #108 arith (- 1) +[attach-meaning] #72 arith (- 1) +[attach-meaning] #72 arith (- 1) +[attach-meaning] #108 arith (- 1) +[attach-meaning] #108 arith (- 1) +[mk-app] #239 Int +[attach-meaning] #239 arith 2 +[mk-app] #240 Int +[attach-meaning] #240 arith 3 +[mk-app] #241 Real +[attach-meaning] #241 arith 2 +[mk-app] #242 Real +[attach-meaning] #242 arith 3 +[mk-app] #243 Int +[attach-meaning] #243 arith 4 +[mk-app] #244 Int +[attach-meaning] #244 arith 5 +[mk-app] #245 Int +[attach-meaning] #245 arith 6 +[mk-app] #246 Int +[attach-meaning] #246 arith 7 +[mk-app] #247 Int +[attach-meaning] #247 arith 8 +[mk-app] #248 Int +[attach-meaning] #248 arith 9 +[mk-app] #249 Int +[attach-meaning] #249 arith 10 +[mk-app] #250 Real +[attach-meaning] #250 arith 4 +[mk-app] #251 Real +[attach-meaning] #251 arith 5 +[mk-app] #252 Int +[attach-meaning] #252 arith 11 +[mk-app] #253 Real +[attach-meaning] #253 arith 6 +[attach-meaning] #5 bv #b1 +[attach-meaning] #6 bv #b0 +[attach-meaning] #5 bv #b1 +[attach-meaning] #6 bv #b0 +[attach-meaning] #5 bv #b1 +[attach-meaning] #6 bv #b0 +[attach-meaning] #5 bv #b1 +[attach-meaning] #6 bv #b0 +[attach-meaning] #72 arith (- 1) +[attach-meaning] #72 arith (- 1) +[mk-app] #109 <= #28 #72 +[mk-app] #110 not #109 +[attach-meaning] #72 arith (- 1) +[mk-app] #115 <= #96 #28 +[mk-app] #116 not #115 +[attach-meaning] #72 arith (- 1) +[mk-app] #118 <= #241 #96 +[mk-app] #120 not #118 +[attach-meaning] #72 arith (- 1) +[attach-meaning] #72 arith (- 1) +[mk-app] #155 <= #28 #28 +[mk-app] #130 not #155 +[eof]