summaryrefslogtreecommitdiff
path: root/test/regress/regress0/get-value-reals.smt2
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2020-08-19 07:08:22 -0700
committerGitHub <noreply@github.com>2020-08-19 09:08:22 -0500
commit41f1a9a0036f3d18ec21ef6005fb218cf704fe60 (patch)
treecc314d03286ff6bbd15c157ae06d7bc436d8f831 /test/regress/regress0/get-value-reals.smt2
parent533f87dc6cf44a7bcb84694a5c21e5280425be93 (diff)
[Regressions] Do not test `--check-proofs` anymore (#4914)
In preparation of removing the old proof module, this commit changes the regression runner to not add the flag --check-proofs anymore when running the regressions.
Diffstat (limited to 'test/regress/regress0/get-value-reals.smt2')
-rw-r--r--test/regress/regress0/get-value-reals.smt21
1 files changed, 0 insertions, 1 deletions
diff --git a/test/regress/regress0/get-value-reals.smt2 b/test/regress/regress0/get-value-reals.smt2
index 6fa542668..09ec0917f 100644
--- a/test/regress/regress0/get-value-reals.smt2
+++ b/test/regress/regress0/get-value-reals.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE:
; EXPECT: sat
; EXPECT: ((pos_int (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_int (/ (- 2) 1)))
(set-info :smt-lib-version 2.0)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback