Type error in generated SMT file from range types
With the file
type t = <range 0 3>
goal g : forall x:t. x = (3:t)
the provers CVC4 and CVC5 and Z3 complain with a typing error in the generated SMT file. The ill-typed generated formula is
(forall ((x t)) (= x 3))
The bug is present both in master branch and in the 1.6.0 release. Suspect: a conflict with the eliminate_literal
transformation and the various remove_unused
-like ones, that may have removed the t'int
projection.
In any case, the SMT2 printer should fail more strongly when attempting to print a range literal.