SMT backend multi transaction counterexample

[leonardoalt]

constructor of C
interface constructor()

creates

    uint x := 0

invariants

    x < 2

behaviour f of C
interface f()

case x == 0:

    storage

        x => 1

behaviour g of C
interface g()

case x == 1:

    storage

        x => 2

============

Invariant "(C.x < 2)" of "C": 



---



---

Counter example found!

SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("C_g_x",1 :: Integer),("C_g_x_post",2 :: Integer),("C_g_CALLER",0 :: Integer),("C_g_CALLVALUE",0 :: Integer),("C_g_CALLDEPTH",0 :: Integer),("C_g_ORIGIN",0 :: Integer),("C_g_BLOCKHASH","" :: String),("C_g_BLOCKNUMBER",0 :: Integer),("C_g_DIFFICULTY",0 :: Integer),("C_g_CHAINID",0 :: Integer),("C_g_GASLIMIT",0 :: Integer),("C_g_COINBASE",0 :: Integer),("C_g_TIMESTAMP",0 :: Integer),("C_g_THIS",0 :: Integer),("C_g_NONCE",0 :: Integer)], modelUIFuns = []}

The counterexample is correct, but not complete. It tells us one step to reach x_post = 2 from x_pre = 1, but I'm wondering if we can get the whole trace. I think one possible way is by running extra queries:

1. Get the cex above, g() makes x_pre = 1 -> x_post = 2
2. Ask how to get to x_post = 1, which gives us f() makes x_pre = 0 -> x_post = 1.
3. Ask how to get to x_post = 0, which gives us init() (or similar) makes x_post = 0

[MrChico]

I think this procedure is a bit broader than just counterexample generation. The procedure you are describing is essentially a backtracing to the initial state from the goal, and so would also be able to discard noninductive invariants which would currently be false positives. For example, if there was no f() spec above, the invariant would actually hold, but the counterexample would still be provided by act prove