2 files changed, 15 insertions, 18 deletions
diff --git a/test/regress/regress0/printer/tuples_and_records.cvc b/test/regress/regress0/printer/tuples_and_records.cvc
deleted file mode 100644
index 966668002..000000000
--- a/test/regress/regress0/printer/tuples_and_records.cvc
+++ /dev/null
@@ -1,18 +0,0 @@
-% EXPECT: not_entailed
-% EXPECT: ((r.a, "active"))
-% EXPECT: ((y.1, 9))
-OPTION "produce-models";
-
-R : TYPE = [#
-   a : STRING,
-   b : STRING
-#];
-r : R;
-
-y: [REAL, INT, REAL];
-
-ASSERT r = (# a := "active", b := "who knows?" #);
-ASSERT y = ( 4/5, 9, 11/9 );
-QUERY r.a = "what?";
-GET_VALUE r.a;
-GET_VALUE y.1;
diff --git a/test/regress/regress0/printer/tuples_and_records.cvc.smt2 b/test/regress/regress0/printer/tuples_and_records.cvc.smt2
new file mode 100644
index 000000000..49d12d1c0
--- /dev/null
+++ b/test/regress/regress0/printer/tuples_and_records.cvc.smt2
@@ -0,0 +1,15 @@
+; EXPECT: sat
+; EXPECT: (((a r) "active"))
+; EXPECT: ((((_ tupSel 1) y) 9))
+(set-logic ALL)
+(set-option :incremental false)
+(set-option :produce-models true)
+(declare-datatypes ((__cvc5_record_a_String_b_String 0)) (((__cvc5_record_a_String_b_String_ctor (a String) (b String)))))
+
+(declare-fun r () __cvc5_record_a_String_b_String)
+(declare-fun y () (Tuple Real Int Real))
+(assert (= r (__cvc5_record_a_String_b_String_ctor "active" "who knows?")))
+(assert (= y (mkTuple (/ 4 5) 9 (/ 11 9))))
+(check-sat-assuming ( (not (= (a r) "what?")) ))
+(get-value ( (a r) ))
+(get-value ( ((_ tupSel 1) y) ))