Polyupdate: state x : Bag<Int> state s : Int query sm() s + sum x op a(y : Int) x.add(y); if (y > 0) { s = s + y; }public void a(Integer y) { Integer _conditional_result345643 = 0; if ((y > 0)) { _conditional_result345643 = (_var23 + y); } else { _conditional_result345643 = _var23; } Integer _var345637 = _conditional_result345643; Integer _var345638 = (_var426 + y); _var23 = _var345637; _var426 = _var345638;}assert(this._var23 == old_this._var23 + y); assert(this._var426 == y + old_this._var426);public Integer sm() { return (_var23 + _var426);}assert(result == this._var23 + this._var426);