MuZ3 is unsound and incomplete as of PRQ #66

[MattWindsor91]

Edit: My incompleteness result here also fails with HSF. Needs further investigation, I suspect it's because setting all variables to 0 refutes emp?

Unsound:

$ ./starling.sh -smusat Examples/Fail/ticketLockBad.cvf
Proof SUCCEEDED.
View assignments:
    (let ((a!1 (forall ((A Int) (B Int)) (= (emp A B) (<= (+ A (* (- 1) B)) 0)))))
      (and (forall ((A Int) (B Int)) (= (v_holdLock A B) true))
           a!1
           (forall ((A Int) (B Int) (C Int)) (= (v_holdLock_holdTick A B C) true))))

Incomplete:

$ ./starling.sh -smusat Examples/Pass/singleWriterMultiReaderLock.cvf
Proof FAILED.
Counter-example:
    true

I'm not sure what is going on here but I suspect our encoding into Horn clauses is wrong.

[MattWindsor91]

Just to confirm, Z3 can do both of these:

$ ./starling.sh -ssmt-failures Examples/Fail/ticketLockBad.cvf
Proof failures:
    unlock_C000_002 fail:
        Could not prove that this command:
            int serving <- !I++ (before serving)
            which was translated into:
                true

        under the weakest precondition:
            <|emp((before serving), (before ticket)); v_holdLock((before serving), (before ticket))|>
            which was translated into:
                (and
                    (>= (before ticket) (before serving))
                    (not (= (before ticket) (before serving)))
                )

        establishes:
            v_holdLock((+ (before serving) 1), (before ticket))
            which was translated into:
                (not (= (before ticket) (+ (before serving) 1)))

    unlock_C000_003 fail:
        Could not prove that this command:
            int serving <- !I++ (before serving)
            which was translated into:
                true

        under the weakest precondition:
            <|emp((before serving), (before ticket)); v_holdLock((before serving), (before ticket)); v_holdLock_holdTick((before serving), (before ticket), (goal 5 t)); v_holdTick((before serving), (before ticket), (goal 5 t))|>
            which was translated into:
                (and
                    (>= (before ticket) (before serving))
                    (not (= (before ticket) (before serving)))
                    (not (= (before serving) (goal 5 t)))
                    (> (before ticket) (goal 5 t))
                )

        establishes:
            v_holdLock_holdTick((+ (before serving) 1), (before ticket), (goal 5 t))
            which was translated into:
                (not (= (+ (before serving) 1) (goal 5 t)))

$ ./starling.sh -ssmt-failures Examples/Pass/singleWriterMultiReaderLock.cvf
No proof failures

[MattWindsor91]

Removing noncritical as we really could do with µZ3 for Paper'17.