From 5ee9b4685a2aeceebeb109b9578be0562efbf700 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 20 Oct 2021 18:31:52 -0700 Subject: [PATCH] Enable and fix dump test (#7387) Fixes #1649. The test was not enabled before and was still expecting CVC-style output. --- test/regress/CMakeLists.txt | 1 + .../regress0/datatypes/datatype-dump.cvc.smt2 | 13 +++++-------- 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fca1543c4..3ea588e01 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -479,6 +479,7 @@ set(regress_0_tests regress0/datatypes/coda_simp_model.smt2 regress0/datatypes/conqueue-dt-enum-iloop.smt2 regress0/datatypes/data-nested-codata.smt2 + regress0/datatypes/datatype-dump.cvc.smt2 regress0/datatypes/datatype.cvc.smt2 regress0/datatypes/datatype0.cvc.smt2 regress0/datatypes/datatype1.cvc.smt2 diff --git a/test/regress/regress0/datatypes/datatype-dump.cvc.smt2 b/test/regress/regress0/datatypes/datatype-dump.cvc.smt2 index f1aae6bb1..7d5495fcc 100644 --- a/test/regress/regress0/datatypes/datatype-dump.cvc.smt2 +++ b/test/regress/regress0/datatypes/datatype-dump.cvc.smt2 @@ -1,14 +1,11 @@ ; COMMAND-LINE: -o raw-benchmark -; EXPECT: OPTION "incremental" false; -; EXPECT: OPTION "logic" "ALL"; -; EXPECT: DATATYPE -; EXPECT: nat = succ(pred: nat) | zero -; EXPECT: END; -; EXPECT: x : nat; -; EXPECT: QUERY NOT(is_succ(x)) AND NOT(is_zero(x)); +; EXPECT: (set-option :incremental false) +; EXPECT: (set-logic ALL) +; EXPECT: (declare-datatypes ((nat 0)) (((succ (pred nat)) (zero)))) +; EXPECT: (declare-fun x () nat) +; EXPECT: (check-sat-assuming ( (not (and (not ((_ is succ) x)) (not ((_ is zero) x)))) )) ; EXPECT: sat (set-logic ALL) -(set-option :incremental false) (declare-datatypes ((nat 0)) (((succ (pred nat)) (zero)))) (declare-fun x () nat) (check-sat-assuming ( (not (and (not ((_ is succ) x)) (not ((_ is zero) x)))) )) -- 2.30.2