Restore record printing functionality

src/lib/frontend/models.ml

@@ -416,7 +416,13 @@ module SmtlibCounterExample = struct
            else
              reps_aux representants
          in
-         print_fun_def fmt f xs_ty_named ty rep;
+         (* Only print declared (but not defined!) function symbols -- note
+            that we still need to *handle* other symbols without printing them
+            because they could be record accessors that must be added to the
+            `records` reference *)
+         match f with
+         | Sy.Name (_, _, false) -> print_fun_def fmt f xs_ty_named ty rep
+         | _ -> ()
       ) fprofs;
     !records
 end

src/lib/reasoners/uf.ml

@@ -1026,7 +1026,9 @@ let compute_concrete_model ({ make; _ } as env) =
   ME.fold
     (fun t _mk ((fprofs, cprofs, carrays, mrepr) as acc) ->
        let { E.f; xs; ty; _ } = E.term_view t in
-       if X.is_solvable_theory_symbol f ty
+       (* Keep record constructors because models.ml expects them to be there *)
+       if (X.is_solvable_theory_symbol f ty
+           && not (Shostak.Records.is_mine_symb f ty))
        || E.is_fresh t || E.is_fresh_skolem t
        || E.equal t E.vrai || E.equal t E.faux
        then

tests/dune.inc

@@ -186828,6 +186828,31 @@
 ; Auto-generated part end
 ; File auto-generated by gentests
 
+; Auto-generated part begin
+(subdir models/records
+  (rule
+   (target record1.models_tableaux.output)
+   (deps (:input record1.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver Tableaux
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff record1.models.expected record1.models_tableaux.output))))
+; Auto-generated part end
+; File auto-generated by gentests
+
 ; Auto-generated part begin
 (subdir models/uf
   (rule

tests/models/records/record1.models.expected

@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun a () Pair (pair 5 0))
+)

tests/models/records/record1.models.smt2

@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-datatype Pair
+((pair (first Int) (second Int))))
+(declare-const a Pair)
+(assert (= (first a) 5))
+(check-sat)
+(get-model)