solve_ndisj: solve more goals involving chains of differences (!300) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Ralf Jung requested to merge ralf/solve_ndisj into master 3 years ago

All threads resolved!

This improves solve_ndisj to handle goals that came up in iris/examples as part of the logically atomic triple mask change.

Approval is optional

Activity

Robbert Krebbers @robbertkrebbers started a thread on the diff 3 years ago

Resolved 3 years ago by Robbert Krebbers
Last reply by Ralf Jung 3 years ago

Ralf Jung mentioned in merge request !301 (merged) 3 years ago

mentioned in merge request !301 (merged)

Ralf Jung added 3 commits 3 years ago

added 3 commits

49d6a4f9...fa9692b2 - 2 commits from branch master
d0176db3 - solve_ndisj: solve more goals involving chains of differences

Compare with previous version

Ralf Jung added 1 commit 3 years ago

added 1 commit

b5adcbea - changelog

Compare with previous version

Robbert Krebbers resolved all threads 3 years ago

resolved all threads

Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 3 years ago

Resolved 3 years ago by Ralf Jung

Robbert Krebbers @robbertkrebbers · 3 years ago

Owner

LGTM.

Ralf Jung resolved all threads 3 years ago

resolved all threads

Ralf Jung added 1 commit 3 years ago

added 1 commit

22a2d166 - more detailed changelog

Compare with previous version

Ralf Jung enabled an automatic merge when the pipeline for succeeds 3 years ago

enabled an automatic merge when the pipeline for 22a2d166 succeeds

Ralf Jung @jung · 3 years ago

Author Owner

@iris-users this again makes solve_ndisj more powerful, so some proofs could break because more goals are closed by this tactic.

Ralf Jung mentioned in commit 3 years ago

mentioned in commit e0de35f0

Ralf Jung merged 3 years ago

merged

Please register or sign in to reply