Define-sort not supported

[bobot]

Sort definition (type alias) seems not supported:

(set-logic QF_LIA)
(define-sort F () Int)
(declare-fun x () F)
(assert (= x 1))
(check-sat)
(exit)

returns:

Error While typing: (= (x) 1)
File ./test.smt2, line 4, character 8-15:
The term: 1 has type int but was expected to be of type F

[Gbury]

Oops, that was an oversight on my part: to have more lightweight type-checking, definitions (including for types, instead of just for terms), are type-checked and then the defined symbol is simply declared, but that's clearly wrong for type definitions.
You'll notice that there already was a builtin functor to handle definitions by substitutions, I just forgot to use it. This should be fixed in #30 .

[bobot]

Thanks for the quick fix and the explanations.