cvc4 errors in local test

[cblp]

Interesting, Travis reports everything is OK, but when I locally run make test or make travis-test I have following 5 errors:

1. should be safe

   1. foo9

      CVC4 Error:
          Parse Error: /tmp/cvc4-inputs/cvc4input18130801541579068977.cvc:43.40: Unexpected token: '['.
      FAIL
          Expected: Safe
          Actual: Error: [] (generated script at /tmp/cvc4-inputs/cvc4input18130801541579068977.cvc)

      Haskell code:

      [ivory|
      struct foo2
      { aFoo :: Stored Uint8
      ; bFoo :: (Array 4 Uint8)
      }
      |]
      
      ...
      store (f ~> bFoo ! 0) 1
      ...

      CVC4 code:

      ...
      ASSERT mc_2var0 = (mc_1var0 WITH .bFoo[0] := 1) ;
      ......................................^

   2. foo18

      FAIL
          Expected: Safe
          Actual: Error: ["expecting an arithmetic subterm"] (generated script at /tmp/cvc4-inputs/cvc4input16717359902010794583.cvc)

2. examples (shouldn't crash)

   1. t1

      CVC4 Error:
          Parse Error: /tmp/cvc4-inputs/cvc4input12678896181326247643.cvc:1055.66: Unexpected token: '.'.
      FAIL (0.02s)
          Expected: anything but Error
          Actual: Error: [] (generated script at /tmp/cvc4-inputs/cvc4input12678896181326247643.cvc)

      Haskell code:

      arrayMap $ \ix ->
        store ((param_info_ref ! ix) ~> param_requested) 1

      CVC4 code:

      ...
      ASSERT mc_1g_param_info = (g_param_info WITH [ix0].param_requested := 1) ;
      .................................................................^

   2. arrayExample

      FAIL
          Expected: anything but Error
          Actual: Error: ["expecting an arithmetic subterm"] (generated script at /tmp/cvc4-inputs/cvc4input1390543437216220853.cvc)

   3. fib_struct_loop

      FAIL (0.14s)
          Expected: anything but Error
          Actual: Error: ["expecting an arithmetic subterm"] (generated script at /tmp/cvc4-inputs/cvc4input1043388777413360099.cvc)

Why it can be?

$ cvc4 --version
This is CVC4 version 1.3
compiled with GCC version 4.7.2
on Dec  7 2013 19:02:28

[leepike]

There are at least two problems right now: (1) there is a known parsing bug in CVC4; that is why Travis pulls down a particular build, and (2) there are some known issues with the symbolic simulator, in general.

I think the thing to do until @eddywestbrook gets a chance to integrate the new symbolic simulator is for me to deprecate the CVC4 for checks in Travis-CI.

[leepike]

Testing on https://github.com/GaloisInc/ivory/tree/deprecate/cvc4 ...

[cblp]

But why? CVC4 works good on Travis!

[leepike]

Oh, ok. We could keep running it on Travis, but as I mentioned, it should be replaced soon anyway.