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

diff --git a/.travis.yml b/.travis.yml
index 61a40a9f6246c92782b91264d4c9bac72da97bd5..40a30b1002ae1a144b1726d9e5bd65b1c4efecb5 100644 (file)
--- 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 d14c63be5250aeecdf88ae76453f3e15a68f9d1b..9509259a4a6af79a941ef0bece0bd4c45e2f3595 100644 (file)
--- 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