You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I have a parameterized property that I want to prove for a bunch of different concrete parameters. For example:
prop : [32] -> [32] -> Bit
prop a b = ...
And I want to prove prop for all a, but where b is a set of concrete values. So, prove \a -> prop a 10 and \a -> prop a 87 and ...
If I put the concrete values of b in a list and do the prove command in a loop, the term to be proved is symbolically executed every call to prove, and symbolic execution takes quite some time, whereas the call to the solver is quick. Is there some way to dump a symbolically executed term to SMTLIB2 and then add some extra constraints, so that symbolic execution is only done once? I have looked at doing this manually (dumping the SMTLIB2 and trying to change the symbolic bits for b to constants, but the SMTLIB2 produced by saw doesn't make the symbols for b readily available.
The text was updated successfully, but these errors were encountered:
It may be that being able to store and re-load a term in either SAWCore or What4 external syntax could provide a solution to this. But #1112 shows that there are some bugs in the SAWCore external format that prevent that from working for this use case at the moment.
I have a parameterized property that I want to prove for a bunch of different concrete parameters. For example:
And I want to prove
prop
for alla
, but whereb
is a set of concrete values. So, prove\a -> prop a 10
and\a -> prop a 87
and ...If I put the concrete values of
b
in a list and do the prove command in a loop, the term to be proved is symbolically executed every call toprove
, and symbolic execution takes quite some time, whereas the call to the solver is quick. Is there some way to dump a symbolically executed term to SMTLIB2 and then add some extra constraints, so that symbolic execution is only done once? I have looked at doing this manually (dumping the SMTLIB2 and trying to change the symbolic bits forb
to constants, but the SMTLIB2 produced bysaw
doesn't make the symbols forb
readily available.The text was updated successfully, but these errors were encountered: