newtype oddint = n:nat | n%2 == 1 witness 1

class StackOdd
{
    var s : seq<int>;

    predicate Valid()
        reads this
    {
        forall k :: 0 <= k < |s| ==> s[k] % 2 == 1
    }

    constructor () 
        ensures Valid()
        ensures |s| == 0
    {
        s := [];
    }

    method pop() returns (n: int)
        requires 0 < |s|
        requires Valid()
        modifies this
        ensures |s| == |old(s)| - 1
        ensures Valid()
    {
        n := s[0];
        s := s[1..];
    }

    method push(n: int)
        modifies this
        requires Valid()
        ensures n%2 == 1 ==> |s| == |old(s)| + 1
        ensures n%2 == 0 ==> |s| == |old(s)|
        ensures Valid()
    {
        if n%2 == 1 
        {
            s := [n] + s;
        }
    }

    method length() returns (n: nat)
        ensures n == |s|
    {
        return |s|;
    }

    method Main()
    {
        var s := new StackOdd();
        s.push(1);
        s.push(2);
        var x := s.pop();
        s.push(3);
        var l := s.length();
        assert l == 1;
    }
}