From ff7d33c2f75668fde0f149943e3cf1bedad1102f Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 5 Aug 2013 18:29:34 -0400
Subject: Proof-checking code; fixups of segfaults and missing functionality in
 proof generation; fix bug 285.

* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
---
 .travis.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to '.travis.yml')

diff --git a/.travis.yml b/.travis.yml
index b8d958ed5..c47ad1928 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -27,7 +27,7 @@ script:
        make -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}DISTCHECK FAILED${normal}"; echo; exit 1);
      else
        (make -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}BUILD/TEST FAILED${normal}"; echo; exit 1)) &&
-       (make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' || (echo; echo "${red}PORTFOLIO TEST FAILED${normal}"; echo; exit 1)) &&
+       (make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' RUN_REGRESSION_ARGS= || (echo; echo "${red}PORTFOLIO TEST FAILED${normal}"; echo; exit 1)) &&
        (make -j2 examples || (echo; echo "${red}COULD NOT BUILD EXAMPLES${normal}"; echo; exit 1));
      fi;
    elif [ -n "$TRAVIS_LFSC" ]; then
-- 
cgit v1.2.3