The comment in ECst>>smt2: calls to investigate why it can happen that the receiver wraps around an EApp. However, after having invested some time into this investigation, I am realizing that the heart of smt2Cast has to do with the Z3 datatypes, which we don't have use right now, so we should come back to this subject then, and pay attention to the following comment in Serialize.hs:
-- | smt2Cast uses the 'as x T' pattern needed for polymorphic ADT constructors
-- like Nil, see `tests/pos/adt_list_1.fq`
smt2Cast :: SymEnv -> Expr -> Sort -> Builder.Builder
smt2Cast env (EVar x) t = smt2Var env x t
smt2Cast env e _ = smt2 env e
The comment in
ECst>>smt2:calls to investigate why it can happen that the receiver wraps around anEApp. However, after having invested some time into this investigation, I am realizing that the heart of smt2Cast has to do with the Z3 datatypes, which we don't have use right now, so we should come back to this subject then, and pay attention to the following comment inSerialize.hs: