MinFinder: handletype T = Native "int" state xs : Bag<T> invariant unique xs; query findmin() assume exists xs; argmin {x -> x.val} xs op chval(x : T, nv : Native "int") assume x in xs; assume x.val != nv; x.val = nv;public T findmin() { return _var811;}assert(old_this._var88 == this._var88); assert(result == this._var811);public void chval(T x, int nv) { T _min293249 = null; Boolean _first293250 = true; for (T _x293251 : _var88) { int _conditional_result293252 = 0; if ((java.util.Objects.equals(_x293251, x))) { _conditional_result293252 = nv; } else { _conditional_result293252 = (_x293251).getVal(); } int _conditional_result293253 = 0; if((java.util.Objects.equals(_min293249, x))){ _conditional_result293253 = nv; } else { _conditional_result293253 = (_min293249).getVal(); } Boolean _v293254; if (_first293250) { _v293254 = true; } else { _v293254 = (_conditional_result293252 < _conditional_result293253); } if (_v293254) { _first293250 = false; _min293249 = _x293251; } } _var811 = _min293249; { // (x).getVal() = nv; } }assert(old_this._var88 == this._var88);