[FPBV] Futures Timeout with MathSat

[Franck Cassez]

in GetValueFPBitVectorTests, some tests may fail when asserting terms (timeout triggers). This happens in FPBV with MathSat:

- [MathSat] configured with Logic: QF_FPBV. Options: List(MODELS) check-sat for bivector term (fp.eq (fp.add RNE x y ) ( (_ to_fp 5 11) RNE 2.219 ) )   can be established *** FAILED ***
[info]   Failure(org.scalatest.exceptions.TestFailedException: Failure(java.util.concurrent.TimeoutException: Futures timed out after [10 milliseconds]) was not equal to Success(Sat())) was not equal to Success(true)
 (FloatingPointBitVector-tests.scala:172)

[Franck Cassez]

Investigate which command triggers the timeout. Candidates are: - init phase - assert command as the timeout for isSat is set to 10 seconds in the test case.

[Franck Cassez]

The tests run in parallel and it may be that 10.seconds is not enough in CI. Next run, try to increase to 20 and see if still fails on Shippable (did not fail on BitBucket).

[Franck Cassez]

[FPBV] Increase default timeout to 25 seconds re #3

→ <<cset e3270522f066>>

[Franck Cassez]

Increase again default timeout.

see #3

→ <<cset 38e157869eae>>

[Franck Cassez]

Use evalInSolverAsSuccessResponse in DeclareFunCmd instead of evalInSolver. Otherwise the error messages from the solvers may be ignored e.g. Success("(error : ...)"). With evalInSolverAsSuccessResponse returns Sucess only if result is (success).

fixes #3

→ <<cset dc4170815e73>>