eliminate_literal, range types and Eprover driver
On the following example, launching Eprover fails with this error message: "internal failure: Failure in transformation eliminate_literal Ident int63'axiom is already declared, with a different declaration"
The SMT solvers work fine.
module A
use import int.Int
use import mach.int.Int63
let test (x:int63) : int63
requires { x < 100 }
= x+1
end
To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information