From 41f1a9a0036f3d18ec21ef6005fb218cf704fe60 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 19 Aug 2020 07:08:22 -0700 Subject: [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. --- test/regress/regress0/bv/ackermann5.smt2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test/regress/regress0/bv/ackermann5.smt2') diff --git a/test/regress/regress0/bv/ackermann5.smt2 b/test/regress/regress0/bv/ackermann5.smt2 index d29311109..240691cd3 100644 --- a/test/regress/regress0/bv/ackermann5.smt2 +++ b/test/regress/regress0/bv/ackermann5.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores ; EXPECT: sat (set-logic QF_UFBV) -- cgit v1.2.3