Commit 7a33011d authored by Matthew Fernandez's avatar Matthew Fernandez
Browse files

juggle SMT test cases to be more effective

Knowing that `|` in Murphi maps to `||` in C, we swap the order of the
conditionals in the forall test cases to *really* force an undefined read if the
entire expression is not optimised to `true`.
parent ab111f8e
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment