From e8a1ba250dc3b36f25fc13aec74670183722b751 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Fri, 10 Jan 2025 16:55:36 -0800 Subject: [PATCH] set universe to zero in mk_subtype_of_unit --- src/smtencoding/FStarC.SMTEncoding.Term.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smtencoding/FStarC.SMTEncoding.Term.fst b/src/smtencoding/FStarC.SMTEncoding.Term.fst index e2d4421b249..646cf33e0fc 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Term.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Term.fst @@ -1175,7 +1175,7 @@ let mk_Valid t = match t.tm with | _ -> mkApp("Valid", [t]) t.rng let mk_unit_type = mkApp("Prims.unit", []) norng -let mk_subtype_of_unit v = mkApp("Prims.subtype_of", [mk_U_unknown;mk_U_unknown;v;mk_unit_type]) v.rng // GE: FIXME +let mk_subtype_of_unit v = mkApp("Prims.subtype_of", [mk_U_zero;mk_U_zero;v;mk_unit_type]) v.rng let mk_HasType v t = mkApp("HasType", [v;t]) t.rng let mk_HasTypeZ v t = mkApp("HasTypeZ", [v;t]) t.rng let mk_IsTotFun t = mkApp("IsTotFun", [t]) t.rng