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/quantifiers/lra-triv-gn.smt2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test/regress/regress0/quantifiers/lra-triv-gn.smt2') diff --git a/test/regress/regress0/quantifiers/lra-triv-gn.smt2 b/test/regress/regress0/quantifiers/lra-triv-gn.smt2 index 1598f7097..7cc9c2ea3 100644 --- a/test/regress/regress0/quantifiers/lra-triv-gn.smt2 +++ b/test/regress/regress0/quantifiers/lra-triv-gn.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --global-negate --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --global-negate --no-check-unsat-cores ; EXPECT: unsat (set-logic LRA) (set-info :status unsat) -- cgit v1.2.3