From 626c6999d77b6e15ddd8dfd2e8c1c674bb947ff2 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Sat, 15 Jun 2024 12:10:51 +0200 Subject: [PATCH 1/2] Simple ADTs with a single constructor are records This PR fixes a bug in `D_cnf` that have been exposed by #1130. Before merging `Enum` into `ADT` the situation was as follows: - simple ADT with several constructors and with at least one payload was sent to the `Adt` theory - simple ADT with several constructors but no payload was sent to `Enum` theory - simple ADT with a single constructor was sent to the `Record` theory. The last corner case includes a corner corner case: An ADT with a single constructor without payload (so basically the unit type with an extra step...) The `D_cnf` included a bug. It produced single constructors without payload of type ADT instead of type record but the check done in `is_mine_symb` prevented from sending it to `Adt`. As I removed this check, we got an assert on the following input: ```smt2 (set-logic ALL) (declare-datatype t ((Record))) (define-fun a () t Record) (check-sat) ``` After this patch, the situation is as follows: - simple ADT with several constructors is sent to the `Adt` theory - simple ADT with only one constructor is sent to the `Record` theory - mutually recursive ADT whose all the types are record is sent to the `Record` theory --- src/lib/frontend/cnf.ml | 2 +- src/lib/frontend/d_cnf.ml | 12 +- src/lib/reasoners/adt.ml | 7 +- src/lib/structures/expr.ml | 2 + src/lib/structures/expr.mli | 1 + tests/dune.inc | 498 ++++++++++++++++++ tests/smtlib/testfile-empty-record.expected | 2 + tests/smtlib/testfile-empty-record.smt2 | 4 + .../testfile-record-in-mr-adts.expected | 2 + tests/smtlib/testfile-record-in-mr-adts.smt2 | 4 + 10 files changed, 528 insertions(+), 6 deletions(-) create mode 100644 tests/smtlib/testfile-empty-record.expected create mode 100644 tests/smtlib/testfile-empty-record.smt2 create mode 100644 tests/smtlib/testfile-record-in-mr-adts.expected create mode 100644 tests/smtlib/testfile-record-in-mr-adts.smt2 diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index cf2e6166b3..be8ba7b116 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -115,7 +115,7 @@ let rec make_term quant_basename t = | TTrecord lbs -> let lbs = List.map (fun (_, t) -> mk_term t) lbs in - E.mk_term (Sy.Op Sy.Record) lbs ty + E.mk_record lbs ty | TTlet (binders, t2) -> let binders = diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 7b3582e86f..6880a3cc52 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -970,8 +970,14 @@ let rec mk_expr E.mk_term sy [] ty | B.Constructor _ -> - let ty = dty_to_ty term_ty in - E.mk_constr (Uid.of_dolmen tcst) [] ty + begin match dty_to_ty term_ty with + | Trecord _ as ty -> + E.mk_record [] ty + | Tadt _ as ty -> + E.mk_constr (Uid.of_dolmen tcst) [] ty + | _ -> + assert false + end | _ -> unsupported "Constant term %a" DE.Term.print term end @@ -1343,7 +1349,7 @@ let rec mk_expr E.mk_term sy l ty | Ty.Trecord _ -> let l = List.map (fun t -> aux_mk_expr t) args in - E.mk_term (Sy.Op Sy.Record) l ty + E.mk_record l ty | _ -> Fmt.failwith "Constructor error: %a does not belong to a record nor an\ diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 9e8a1e3d94..834ea2ce31 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -193,8 +193,11 @@ module Shostak (X : ALIEN) = struct if equal sel (embed sel_x) then X.term_embed t, ctx else sel_x, ctx (* canonization OK *) *) - | _ -> - assert false + + | Sy.Op Sy.Constr _, _, Ty.Trecord _ -> + Fmt.failwith "unexpected record constructor %a@." E.print t + + | _ -> assert false let hash x = abs @@ match x with diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index b7ae778090..cdccd3baa6 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -1264,6 +1264,8 @@ let mk_constr cons xs ty = mk_term (Sy.Op (Constr cons)) xs ty let mk_tester cons t = mk_builtin ~is_pos:true (Sy.IsConstr cons) [t] +let mk_record xs ty = mk_term (Sy.Op Record) xs ty + (** Substitutions *) let is_skolem_cst v = diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index 4922692f9c..a63ff116a1 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -282,6 +282,7 @@ val mk_ite : t -> t -> t -> t val mk_constr : Uid.t -> t list -> Ty.t -> t val mk_tester : Uid.t -> t -> t +val mk_record : t list -> Ty.t -> t (** Substitutions *) diff --git a/tests/dune.inc b/tests/dune.inc index e40934009a..c379f6a83d 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -207027,6 +207027,255 @@ (package alt-ergo) (action (diff testfile-reset.dolmen.expected testfile-reset.dolmen_dolmen.output))) + (rule + (target testfile-record-in-mr-adts_ci_cdcl_no_minimal_bj.output) + (deps (:input testfile-record-in-mr-adts.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) + (rule + (deps testfile-record-in-mr-adts_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-record-in-mr-adts.expected testfile-record-in-mr-adts_ci_cdcl_no_minimal_bj.output))) + (rule + (target testfile-record-in-mr-adts_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input testfile-record-in-mr-adts.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps testfile-record-in-mr-adts_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-record-in-mr-adts.expected testfile-record-in-mr-adts_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target testfile-record-in-mr-adts_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input testfile-record-in-mr-adts.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps testfile-record-in-mr-adts_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-record-in-mr-adts.expected testfile-record-in-mr-adts_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target testfile-record-in-mr-adts_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input testfile-record-in-mr-adts.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps testfile-record-in-mr-adts_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-record-in-mr-adts.expected testfile-record-in-mr-adts_ci_no_tableaux_cdcl_in_instantiation.output))) + (rule + (target testfile-record-in-mr-adts_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input testfile-record-in-mr-adts.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) + (rule + (deps testfile-record-in-mr-adts_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-record-in-mr-adts.expected testfile-record-in-mr-adts_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) + (rule + (target testfile-record-in-mr-adts_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input testfile-record-in-mr-adts.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) + (rule + (deps testfile-record-in-mr-adts_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-record-in-mr-adts.expected testfile-record-in-mr-adts_ci_tableaux_cdcl_no_minimal_bj.output))) + (rule + (target testfile-record-in-mr-adts_cdcl.output) + (deps (:input testfile-record-in-mr-adts.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) + (rule + (deps testfile-record-in-mr-adts_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-record-in-mr-adts.expected testfile-record-in-mr-adts_cdcl.output))) + (rule + (target testfile-record-in-mr-adts_tableaux_cdcl.output) + (deps (:input testfile-record-in-mr-adts.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) + (rule + (deps testfile-record-in-mr-adts_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-record-in-mr-adts.expected testfile-record-in-mr-adts_tableaux_cdcl.output))) + (rule + (target testfile-record-in-mr-adts_tableaux.output) + (deps (:input testfile-record-in-mr-adts.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (deps testfile-record-in-mr-adts_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-record-in-mr-adts.expected testfile-record-in-mr-adts_tableaux.output))) + (rule + (target testfile-record-in-mr-adts_dolmen.output) + (deps (:input testfile-record-in-mr-adts.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-record-in-mr-adts_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-record-in-mr-adts.expected testfile-record-in-mr-adts_dolmen.output))) + (rule + (target testfile-record-in-mr-adts_fpa.output) + (deps (:input testfile-record-in-mr-adts.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) + (rule + (deps testfile-record-in-mr-adts_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-record-in-mr-adts.expected testfile-record-in-mr-adts_fpa.output))) (rule (target testfile-quoted1.dolmen_dolmen.output) (deps (:input testfile-quoted1.dolmen.smt2)) @@ -207486,6 +207735,255 @@ (package alt-ergo) (action (diff testfile-exit.dolmen.expected testfile-exit.dolmen_dolmen.output))) + (rule + (target testfile-empty-record_ci_cdcl_no_minimal_bj.output) + (deps (:input testfile-empty-record.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) + (rule + (deps testfile-empty-record_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-empty-record.expected testfile-empty-record_ci_cdcl_no_minimal_bj.output))) + (rule + (target testfile-empty-record_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input testfile-empty-record.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps testfile-empty-record_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-empty-record.expected testfile-empty-record_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target testfile-empty-record_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input testfile-empty-record.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps testfile-empty-record_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-empty-record.expected testfile-empty-record_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target testfile-empty-record_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input testfile-empty-record.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps testfile-empty-record_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-empty-record.expected testfile-empty-record_ci_no_tableaux_cdcl_in_instantiation.output))) + (rule + (target testfile-empty-record_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input testfile-empty-record.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) + (rule + (deps testfile-empty-record_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-empty-record.expected testfile-empty-record_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) + (rule + (target testfile-empty-record_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input testfile-empty-record.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) + (rule + (deps testfile-empty-record_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-empty-record.expected testfile-empty-record_ci_tableaux_cdcl_no_minimal_bj.output))) + (rule + (target testfile-empty-record_cdcl.output) + (deps (:input testfile-empty-record.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) + (rule + (deps testfile-empty-record_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-empty-record.expected testfile-empty-record_cdcl.output))) + (rule + (target testfile-empty-record_tableaux_cdcl.output) + (deps (:input testfile-empty-record.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) + (rule + (deps testfile-empty-record_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-empty-record.expected testfile-empty-record_tableaux_cdcl.output))) + (rule + (target testfile-empty-record_tableaux.output) + (deps (:input testfile-empty-record.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (deps testfile-empty-record_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-empty-record.expected testfile-empty-record_tableaux.output))) + (rule + (target testfile-empty-record_dolmen.output) + (deps (:input testfile-empty-record.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-empty-record_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-empty-record.expected testfile-empty-record_dolmen.output))) + (rule + (target testfile-empty-record_fpa.output) + (deps (:input testfile-empty-record.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) + (rule + (deps testfile-empty-record_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-empty-record.expected testfile-empty-record_fpa.output))) (rule (target testfile-echo2.dolmen_dolmen.output) (deps (:input testfile-echo2.dolmen.smt2)) diff --git a/tests/smtlib/testfile-empty-record.expected b/tests/smtlib/testfile-empty-record.expected new file mode 100644 index 0000000000..a6e005255c --- /dev/null +++ b/tests/smtlib/testfile-empty-record.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/smtlib/testfile-empty-record.smt2 b/tests/smtlib/testfile-empty-record.smt2 new file mode 100644 index 0000000000..3c47be278c --- /dev/null +++ b/tests/smtlib/testfile-empty-record.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL) +(declare-datatype t ((Record))) +(define-fun a () t Record) +(check-sat) diff --git a/tests/smtlib/testfile-record-in-mr-adts.expected b/tests/smtlib/testfile-record-in-mr-adts.expected new file mode 100644 index 0000000000..a6e005255c --- /dev/null +++ b/tests/smtlib/testfile-record-in-mr-adts.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/smtlib/testfile-record-in-mr-adts.smt2 b/tests/smtlib/testfile-record-in-mr-adts.smt2 new file mode 100644 index 0000000000..17a1778488 --- /dev/null +++ b/tests/smtlib/testfile-record-in-mr-adts.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL) +(declare-datatypes ((u 0) (v 0)) (((Record)) ((C) (D)))) +(define-fun a () u Record) +(check-sat) From baa78f1dd3cd58c6ae4cffb29c0252e588772661 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 17 Jun 2024 23:32:38 +0200 Subject: [PATCH 2/2] Tunit is a special case --- src/lib/frontend/d_cnf.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 6880a3cc52..96df62c1bb 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -975,8 +975,10 @@ let rec mk_expr E.mk_record [] ty | Tadt _ as ty -> E.mk_constr (Uid.of_dolmen tcst) [] ty - | _ -> - assert false + | Tunit -> + E.void + | ty -> + Fmt.failwith "unexpected type %a@." Ty.print ty end | _ -> unsupported "Constant term %a" DE.Term.print term