From 29b2e5a74eb007f04a18e01d7a9c21eff577c9b1 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 20 Aug 2018 20:23:09 -0700 Subject: Remove support for *.expect files in regressions (#2341) Currently, we can optionally specify an *.expect file with the metadata of a regression test. This commit removes that option because it was not widely used, adds maintenance overhead and makes the transition to a new build system more cumbersome. Regression files can still be fed to a solver without removing the metadata first since they are in comments of the corresponding input format (note that this was not always the case, it changed in efc6163629c6c5de446eccfe81777c93829995d5). --- test/regress/regress1/push-pop/bug216.smt2 | 4 ++++ test/regress/regress1/push-pop/bug216.smt2.expect | 3 --- 2 files changed, 4 insertions(+), 3 deletions(-) delete mode 100644 test/regress/regress1/push-pop/bug216.smt2.expect (limited to 'test/regress/regress1/push-pop') diff --git a/test/regress/regress1/push-pop/bug216.smt2 b/test/regress/regress1/push-pop/bug216.smt2 index 78e0f716c..53f4fac9c 100644 --- a/test/regress/regress1/push-pop/bug216.smt2 +++ b/test/regress/regress1/push-pop/bug216.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat + (set-logic QF_UF) (declare-fun x () Bool) (declare-fun y () Bool) diff --git a/test/regress/regress1/push-pop/bug216.smt2.expect b/test/regress/regress1/push-pop/bug216.smt2.expect deleted file mode 100644 index fe118171a..000000000 --- a/test/regress/regress1/push-pop/bug216.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: sat -% EXPECT: unsat -- cgit v1.2.3