In the discussion on MFGs, the one of the functions converted is written below:

``````int simple_conditional(int x) {
if (x != 0) {
return 1;
} else {
return 0;
}
}
``````

Which was then converted to:

Now we want to take that MFG and turn it into something we can use to prove things about this function. To do so, we convert our MFG into a series of SMT statements.

To do so, we can fairly trivially define most of the operators in our graph using built in operators in SMT compatible languages. Similarly, psi nodes are quite simple to define: a psi node is true if all its inputs are true, and the truthiness of a psi node implies its output. In this manner, we can weakly define variables and let the eventual consistency of the control flow handle making sure only one of them are true.

``````(declare-fun x () Int)
(declare-fun psi-1 () Bool)
(declare-fun psi-2 () Bool)
(declare-fun ret () Int)
(assert (= psi-1 (not (= x 0))))
(assert (=> psi-1 (= ret 1)))
(assert (= psi-2 (not psi-1)))
(assert (=> psi-2 (= ret 0)))
``````

Now that we've defined our function in SMT statements, we can even evaluate over our function using an SMT solver. Fun!

``````(declare-fun x () Int)
(declare-fun psi-1 () Bool)
(declare-fun psi-2 () Bool)
(declare-fun ret () Int)
(assert (= psi-1 (not (= x 0))))
(assert (=> psi-1 (= ret 1)))
(assert (= psi-2 (not psi-1)))
(assert (=> psi-2 (= ret 0)))

(push)
(assert (= x 1))

(check-sat)
(get-model)

(pop)
(push)
(assert (= x 0))

(check-sat)
(get-model)
(pop)
``````

You can go ahead and try this using Microsoft's online Z3 evaluator.

You can even do this with larger examples, like the `complex_conditional` exhibited in the discussion on MFGs, but I leave that as an exercise to the reader for now.