From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Sat, 18 May 2019 22:13:00 +0000 (-0700)
Subject: FP: Fix regression test and enable SymFPU on Travis. (#3013)
X-Git-Tag: cvc5-1.0.0~4140
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5fcb1dd18bf01a95198c4981e2d81da64f5a4848;p=cvc5.git

FP: Fix regression test and enable SymFPU on Travis. (#3013)
---

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