SMT backend multi transaction counterexample

```
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`

Start by tracing the SMT backend's counterexample query for the shown C contract. Check whether follow-up queries can recover the g, f, and init transitions in order; done means outputting a complete trace rather than only the g() step.

Written by the indexing model from the issue text.