|
|
|
|
|
|
by rurban
4097 days ago
|
|
|
Then rather use cmbc, which does exactly that. It translates C code into SMT rules, allows assertions on symbolic variables and solves them.
And note that for harder crypto problems Z3 is not the best, it's just the easiest to use. |
|
|