MaxBag: state l : Set<Int> query get_max() assume exists l; argmax {x -> x} l op add(x: Int) assume not(x in l); l.add(x); op remove(x: Int) l.remove(x);public Integer get_max() { return _var587;}assert(!(this._var4384 == null)); assert(old_this._var5992 == this._var5992); assert(old_this._var721 == this._var721); assert(result == this._var587); assert(old_this._var1457 == this._var1457); assert(old_this._var66253 == this._var66253);public void add(Integer x) { Integer _conditional_result328431 = 0; if (_var1457) { Integer _conditional_result328432 = 0; if ((_var587 > x)) { _conditional_result328432 = _var587; } else { _conditional_result328432 = x; } _conditional_result328431 = _conditional_result328432; } else { _conditional_result328431 = x; } Integer _var328366 = _conditional_result328431; Integer _var328367 = (_var5992 + 1); _var587 = _var328366; _var1457 = true; Integer _heap_size328371 = _var5992; Integer _heap_size328376 = _var5992; for (;;) { Boolean _v328434; if ((((_heap_size328376 + 1) - 1) >= 0)) { Boolean _v328435; if ((((_heap_size328376 + 1) - 1) >= 0)) { _v328435 = (((_heap_size328376 + 1) - 1) < ((_var4384)._1.length)); } else { _v328435 = false; } _v328434 = (!(_v328435)); } else { _v328434 = false; } if ((!(_v328434))) { break; } Integer[] _new_array328433 = new Integer[(((_var4384)._1.length) << 1) + 1]; System.arraycopy((_var4384)._1, 0, _new_array328433, 0, ((_var4384)._1.length)); (_var4384)._1 = _new_array328433; } { (_var4384)._0 = ((_var4384)._0 + 1); (_var4384)._1[_heap_size328376] = x; Integer _i328377 = _heap_size328376; for (;;) { Boolean _v328436; if ((_i328377 > 0)) { _v328436 = (!(((_var4384)._1[((_i328377 - 1) >> 1)] >= (_var4384)._1[_i328377]))); } else { _v328436 = false; } if ((!(_v328436))) { break; } Integer _swap_tmp328437 = (_var4384)._1[((_i328377 - 1) >> 1)]; (_var4384)._1[((_i328377 - 1) >> 1)] = (_var4384)._1[_i328377]; (_var4384)._1[_i328377] = _swap_tmp328437; _i328377 = ((_i328377 - 1) >> 1); } _heap_size328376 = (_heap_size328376 + 1); } { _var66253.add(x); } _var5992 = _var328367; { Boolean _var1233 = _var721.getOrDefault(x, false); _var1233 = true; _var721.put(x, _var1233); } }assert(old_this._var587 != this._var587 + 2); assert(old_this._var5992 != this._var5992 + this._var587 - x); assert(old_this._var5992 <= this._var5992 + this._var587 - x); assert(!(this._var721 == null)); assert(old_this._var5992 >= this._var5992 - 1); assert(old_this._var5992 != this._var5992 + old_this._var5992 + 1); assert(this._var721 != null); assert(!(this._var66253 == null)); assert(ExpressionEvaluator.evaluateSetMembership(x,"this . _var66253",this)); assert(old_this._var5992 != this._var5992); assert(old_this._var66253 != this._var66253); assert(old_this._var587 != this._var587 + 1); assert(ExpressionEvaluator.evaluateSetMembership(x,"this . _var721 . keySet",this)); assert(this._var587 == this._var587); assert(old_this._var5992 == this._var5992 - 1); assert(!(this._var4384 == null)); assert(this._var1457 == true); assert(old_this._var5992 <= this._var5992); assert(old_this._var4384 != this._var4384); assert(old_this._var5992 != this._var5992 + 1);public void remove(Integer x) { Integer _conditional_result328438 = 0; if ((java.util.Objects.equals(x, _var587))) { Integer _var328379 = 0; switch ((_var4384)._0) { case 0: _var328379 = 0; break; case 1: _var328379 = 0; break; case 2: _var328379 = (_var4384)._1[1]; break; default: Integer _conditional_result328439 = 0; if (((_var4384)._1[1] > (_var4384)._1[2])) { _conditional_result328439 = (_var4384)._1[1]; } else { _conditional_result328439 = (_var4384)._1[2]; } _var328379 = _conditional_result328439; } _conditional_result328438 = _var328379; } else { _conditional_result328438 = _var587; } Integer _var328368 = _conditional_result328438; Integer _sum328440 = 0; if (_var721.containsKey(x)) { { { _sum328440 = (_sum328440 + 1); } } } Integer _var328369 = (_var5992 - _sum328440); java.util.ArrayList<Integer> _conditional_result328443 = new java.util.ArrayList<Integer>(); if (_var721.containsKey(x)) { java.util.ArrayList<Integer> _singleton328448 = new java.util.ArrayList<Integer>(); _singleton328448.add(x); _conditional_result328443 = _singleton328448; } else { _conditional_result328443 = new java.util.ArrayList<Integer>(); } java.util.ArrayList<Integer> _var328370 = _conditional_result328443; _var587 = _var328368; Integer _conditional_result328444 = 0; java.util.ArrayList<Integer> _singleton328449 = new java.util.ArrayList<Integer>(); _singleton328449.add(x); if (((_var66253 == _singleton328449))) { _conditional_result328444 = 1; } else { _conditional_result328444 = 0; } _var1457 = (_var5992 > _conditional_result328444); Integer _heap_size328380 = _var5992; if (_var721.containsKey(x)) { { (_var4384)._0 = ((_var4384)._0 - 1); Integer _i328381 = (java.util.Arrays.asList((_var4384)._1).indexOf(x)); Integer _swap_tmp328450 = (_var4384)._1[_i328381]; (_var4384)._1[_i328381] = (_var4384)._1[(_heap_size328380 - 1)]; (_var4384)._1[(_heap_size328380 - 1)] = _swap_tmp328450; _stop_bubble_down328383: do { for (;;) { if ((!((((_i328381 << 1) + 1) < (_heap_size328380 - 1))))) { break; } Integer _child_index328384 = ((_i328381 << 1) + 1); Boolean _v328451; if ((((_i328381 << 1) + 2) < (_heap_size328380 - 1))) { _v328451 = (!(((_var4384)._1[((_i328381 << 1) + 1)] >= (_var4384)._1[((_i328381 << 1) + 2)]))); } else { _v328451 = false; } if (_v328451) { _child_index328384 = ((_i328381 << 1) + 2); } if ((!(((_var4384)._1[_i328381] >= (_var4384)._1[_child_index328384])))) { Integer _swap_tmp328452 = (_var4384)._1[_i328381]; (_var4384)._1[_i328381] = (_var4384)._1[_child_index328384]; (_var4384)._1[_child_index328384] = _swap_tmp328452; _i328381 = _child_index328384; } else { break _stop_bubble_down328383; } } } while (false); _heap_size328380 = (_heap_size328380 - 1); } } Integer _sum328445 = 0; if (_var721.containsKey(x)) { { { _sum328445 = (_sum328445 + 1); } } } Integer _heap_size328385 = (_var5992 - _sum328445); for (;;) { Boolean _v328454; if ((((_heap_size328385 + 0) - 1) >= 0)) { Boolean _v328455; if ((((_heap_size328385 + 0) - 1) >= 0)) { _v328455 = (((_heap_size328385 + 0) - 1) < ((_var4384)._1.length)); } else { _v328455 = false; } _v328454 = (!(_v328455)); } else { _v328454 = false; } if ((!(_v328454))) { break; } Integer[] _new_array328453 = new Integer[(((_var4384)._1.length) << 1) + 1]; System.arraycopy((_var4384)._1, 0, _new_array328453, 0, ((_var4384)._1.length)); (_var4384)._1 = _new_array328453; } if (_var721.containsKey(x)) { { _var66253.remove(x); } } _var5992 = _var328369; for (Integer _var3237 : _var328370) { _var721.remove(_var3237); } }assert(this._var5992 <= old_this._var5992); assert(x != old_this._var587 + x + 1 - this._var587); assert(old_this._var4384 != this._var4384); assert(!(this._var4384 == null)); assert(!(this._var66253 == null)); assert(old_this._var5992 <= this._var5992 + 1); assert(this._var721 != null);