'How to put SSA in the Z3 solver

I generated the SSA list for my code and now would love to solve the paths from entry to exit. Lets take this "simple" example of SSA expressions.

enter image description here

So then I would have a bunch of expressions:

z1>1
x1:=1
z1>2
x2:=2
y1:=x1+1
x3:=Φ(x1,x2)
z2:=x3-3
x4:=4
z3:=x4+7

However looking at the Z3 examples I cannot directly plug this into the solver, and instead have to generate symbols for them, moreover it seems assignments are not allowed seperately (like x4:=4).

So I wonder if there is any easy way to convert SSAs like above such that I can directly put them in python Z3 solver?

algorithmz3solverz3py


Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source

Related Questions