cvc5 / LFSC

LFSC Proof Checker
Other
11 stars 9 forks source link

Remove compare primitive #73

Open ajreynol opened 2 years ago

ajreynol commented 2 years ago

See discussion on https://github.com/cvc5/LFSC/issues/70.

Fixes https://github.com/cvc5/LFSC/issues/70.

ajreynol commented 2 years ago

Hm, seems compare was used in another signature that is in one of our tests.

alex-ozdemir commented 2 years ago

Yes, but feel free to cut the necessary tests. Our old test suite included a bunch of proofs under the old signature.

alex-ozdemir commented 2 years ago

Speaking of which, it would be good to generate some new tests from the new signatures :)