Prime missing from mutable axioms in SAT checker

[edenfrenkel]

Shouldn't there be a prime added to the mutable axioms in the line below? I think that the idea was to add all axioms to the initial states, and then only the mutable ones to post-states of a transition.

https://github.com/vmware-research/temporal-verifier/blob/343eb699ccbec27620c4002089554ffeeb97efd8/bounded/src/sat.rs#L42

[edenfrenkel]

This also appears to be the case in bdd.rs and smt.rs:

https://github.com/vmware-research/temporal-verifier/blob/343eb699ccbec27620c4002089554ffeeb97efd8/bounded/src/bdd.rs#L66

https://github.com/vmware-research/temporal-verifier/blob/343eb699ccbec27620c4002089554ffeeb97efd8/bounded/src/smt.rs#L29

[Alex-Fischman]

Seems like a bug. Is there a simple test we could add to check that it's wrong?

[odedp]

I'm not even sure we mean to support mutable axioms, but the idea would be something like:

mutable p: bool
mutable q: bool

assume always q <-> p # mutable axiom
assume p # init
assume always p' <-> (p & q) # tr
assert always p # safety