Smt fix #55
Smt fix #55
Conversation
| @@ -187,10 +186,6 @@ let prepreproc sq = | |||
| let hs,_ = List.split res in | |||
| Smt.record_signatures := hs :: !Smt.record_signatures; | |||
| Record (List.map (fun (s, e) -> (s, self#expr scx e)) res) @@ e | |||
| | Apply ({core = Internal B.Eq}, [x ; {core = Internal (B.TRUE | B.FALSE)} as y]) | |||
There was a problem hiding this comment.
I believe you disabled this rewrite because = and <=> have different strength and so there could be an unsoundness if the rewrite was applied to formulas with unsuitable polarity? Would you mind leaving a comment in the code just as you explained the removal of the rewrite about CHOOSE?
There was a problem hiding this comment.
That change was not me, but your explanation is correct. To be even more precise, the core issue is the fact that "x <=> FALSE" is weaker than "x = FALSE". For "TRUE", the two statements are actually equivalent, so I re-included that part of the rewriting rule.
Would be better to keep this rule enabled for negative contexts (for ex. on equality hypotheses), but that would imply making changes everywhere in the SMT code.
This reverts commit a2e46fd. One case of the rule is sound, and I added a comment
The error was in using the term unspec(f, x) in place of unspec([ f EXCEPT ![y] = ex ], x). That rule would allow one to prove obligations without checking the condition x \in DOMAIN f.
This bug was corrected already in two places in the code, one in smt/rewrite, the other in smt/typ_t. There was a third place to correct.
|
Rebased onto main. |
This reverts commit 98556bb, reversing changes made to dc344b6. Signed-off-by: Andrew Helwer <[email protected]>
|
@damiendoligez since this is causing a failing test can it be reverted so that the main branch has all tests pass in the CI? It can be merged again when it doesn't cause a test to fail. |
|
It would be better to merge #98 instead of reverting this PR. |
Contains two soundness fixes for the SMT backend