search

cvc5 / LFSC

LFSC Proof Checker
Other
11 stars 9 forks source link

Using "@" in signatures makes type mismatch #2

Open yoni206 opened 6 years ago

yoni206 commented 6 years ago

When using "@" inside a signature, there is a mismatch between the computed and expected types.

Example (the content of tmp.plf appears below):

$ lfscc sat.plf smt.plf tmp.plf tmp.plf, line 11, column 10: The type expected for an application does not match the computed type.

  1. The expected type: (th_holds (= 0x22a7fb0 0x22a7f50 0x22a7f50))
  2. The computed type: (th_holds (= 0x22a7fb0 0x2273880 0x2273880))

When replacing "(th_holds (= s tt tt))" with "(th_holds (= s t t))", the check is successful (no need to remove the "@" line).

tmp.plf

(declare tmp (! s sort (! t (term s) (@ tt t (th_holds (= s tt tt))))))

(check (% s sort (% t (term s) (: (th_holds (= s t t)) (tmp s t))))))