Ben Rodes

I went directly to using their python api. It appears to be mostly inline with the SWIG api. I started to modify my own fork of pysmt, and for the...

Also, in case anyone finds these messages in the future. You can't simply update CVC4 in pysmt. Changes to their underlying API is no longer working with SWIG. I saw...

I should've updated this thread. After I submitted this report several months ago, I went in and manually modified the theories logic include some of the array-supporting theories I needed...

Thanks @MathiasVP I'll experiment with this a bit. I'm totally unfamiliar with the GlobalValueNumbering module. Sounds like SSA. I'll have to do a bit of research.

My only general concern is if this approach will work for more complex control flow with respect to calculating the guard. The example I gave was purposefully simplified.

Here's an example of what I mean by more complex flow where I'm not sure how to apply the global value numbering solution yet. In my solution I've defined a...

For more context, this is the style of barrier guard I was using. I had to define my own extension of GuardCondition to ensure I got the full guarding condition,...

Thinking on this more, it just seems like the global value solution will eventually require me to make a separate data trace since the values in my examples may flow...

Final thought. If a data path must be considered into the guard as well, then it is also unclear if there is any way to establish the isValid or isInvalid...

Alright, I think I have a way forward here. I've applied your global value numbering solution into my isValid and isInvalid predicates I mentioned. I've updated them to not only...