diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-05-18 15:13:00 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-05-18 15:13:00 -0700 |
| commit | 5fcb1dd18bf01a95198c4981e2d81da64f5a4848 (patch) | |
| tree | 4cc47283e1f4471e52618149c8091d30cc934b0d | |
| parent | 3d79c9b5813eda2f6f55822e193e36a660435e10 (diff) | |
FP: Fix regression test and enable SymFPU on Travis. (#3013)
| -rw-r--r-- | .travis.yml | 9 | ||||
| -rw-r--r-- | test/regress/regress0/fp/down-cast-RNA.smt2 | 2 |
2 files changed, 7 insertions, 4 deletions
diff --git a/.travis.yml b/.travis.yml index 61a40a9f6..40a30b100 100644 --- a/.travis.yml +++ b/.travis.yml @@ -81,9 +81,12 @@ script: $1 || exit 1 echo "travis_fold:end:$1" } + [[ "$TRAVIS_CVC4_CONFIG" == *"symfpu"* ]] && CVC4_SYMFPU_BUILD="yes" + [ -n "$CVC4_SYMFPU_BUILD" ] && run contrib/get-symfpu [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_WITH_LFSC" ] && run contrib/get-lfsc-checker [ -n "$TRAVIS_CVC4" ] && run configureCVC4 - [ -n "$TRAVIS_CVC4" ] && run makeCheck && run makeInstallCheck + [ -n "$TRAVIS_CVC4" ] && run makeCheck + [ -z "$CVC4_SYMFPU_BUILD" ] && run makeInstallCheck [ -z "$TRAVIS_CVC4" ] && error "Unknown Travis-CI configuration" echo "travis_fold:end:load_script" - echo; echo "${green}EVERYTHING SEEMED TO PASS!${normal}" @@ -97,13 +100,13 @@ matrix: - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='production --language-bindings=java --lfsc' - compiler: gcc env: - - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='debug --lfsc --no-debug-symbols' + - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='debug --symfpu --lfsc --no-debug-symbols' # # Test with Clang - compiler: clang env: - - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='debug --cln --gpl --no-debug-symbols --no-proofs' + - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='debug --symfpu --cln --gpl --no-debug-symbols --no-proofs' notifications: email: on_success: change diff --git a/test/regress/regress0/fp/down-cast-RNA.smt2 b/test/regress/regress0/fp/down-cast-RNA.smt2 index d14c63be5..9509259a4 100644 --- a/test/regress/regress0/fp/down-cast-RNA.smt2 +++ b/test/regress/regress0/fp/down-cast-RNA.smt2 @@ -9,7 +9,7 @@ (set-info :status unsat) (declare-fun r () (_ FloatingPoint 5 9)) -(declare-fun rr () (_ FloatingPoint 5 9) ((_ to_fp 5 9) RNA (fp #b1 #b00000 #b1111111110))) +(define-fun rr () (_ FloatingPoint 5 9) ((_ to_fp 5 9) RNA (fp #b1 #b00000 #b1111111110))) ; Let's work out this one out manually ; #b1111111110 is an significand of |