added type signatures
o Added some exception handling to the multithreaded prover in order to transmit exceptions from the workers to the caller
o Added some type signatures
o added type signatures
o removed the array type constructor
added type signatures
Changed the definition of Expr and Type to generalize.
o There are now AbsExpr t (standing for abstract expression relative to type system t) and AbsType t
o Expr and Type are aliases for (AbsExpr GenericType) and GenericType
o Similarly, FOExpr stands for (AbsExpr FOType) with FO standing for First Order, i.e. no genericity
o This allows us to distinguish the language read in the input from the language read by Z3
o The type checker now enforces the requirement of translating from the generic type system to the first-order system