search

smtcoq / sniper

Other
35 stars 6 forks source link

[WIP] example of a confluence proof #11

Closed pi8027 closed 2 years ago

pi8027 commented 2 years ago

Here is the example I wish to prove using Trakt, Sniper, and SMTCoq. My attempt is unsuccessful for the moment.

pi8027 commented 2 years ago

If I need this combination of tools, should I actually use the with-trakt branch? Does scope; trakt Z Prop; smt also work?

pi8027 commented 2 years ago

It seems that I also have to extend prod_of_symb, but could not find the right interface to do so.

pi8027 commented 2 years ago

FTR, I had to use the with-trakt branches of SMTCoq and Sniper, Trakt version 1.0 (1.1 and master does not work), and veriT 9f48a98. It seems that installing the right versions of tools was the most difficult part. ;-)