svQuickCheck weird behavior

[LeventErkok]

@brianhuffman

Consider:

import Data.SBV
import Data.SBV.Dynamic
import Test.QuickCheck

f :: Predicate
f = do x <- sInteger "x"
       let lhs = x + x
           rhs = x * 2
       return $ lhs .== rhs

g :: Symbolic SVal
g = do x <- svMkSymVar Nothing KUnbounded (Just "x")
       let lhs = x `svPlus` x
           rhs = x `svTimes` svInteger KUnbounded 2
       return $ lhs `svEqual` rhs

main :: IO ()
main = do putStrLn "Testing f: "
          quickCheck f
          putStrLn "==========="
          putStrLn "Testing g: "
          _ <- svQuickCheck g
          return ()

I get:

*Main> main
Testing f:
+++ OK, passed 100 tests.
===========
Testing g:
+++ OK, passed 1 tests.

Note that f and g should be equivalent; first coded in the usual style, second coded in the Dynamic style. But for some reason svQuickCheck is only running 1 test. Why is that?

[LeventErkok]

Interesting! I tested this on a different machine; and both actually run 100 tests. The working configuration has the following dependencies:

WORKING$ ghc-pkg field sbv depends
depends:
    QuickCheck-2.9.2-3a8nWdLsV8cEn9LdMoftRm array-0.5.1.1
    async-2.1.0-J6Pl8k3L4PKGEpjYdgwiIf base-4.9.0.0
    base-compat-0.9.1-tmPpmtbHbvIDjFWbkjGrR containers-0.5.7.1
    crackNum-1.5-8XnlQzneC0uH5i3xGn7nTX
    data-binary-ieee754-0.4.4-F1HjhwdV1xx5grS0eMjeg2 deepseq-1.4.2.0
    directory-1.2.6.2 filepath-1.4.1.0 ghc-8.0.1
    mtl-2.2.1-6qsR1PHUy5lL47Hpoa4jCM
    old-time-1.1.0.3-IcvdkJUsE9M8t3io8peAEp pretty-1.1.3.3
    process-1.4.2.0 random-1.1-54KmMHXjttlERYcr1mvsAe
    syb-0.6-C65vWCsht6A8uLstpQIXyj

Would be good to compare this to the dependency list on the failing machine; which I do not have access to right now.

[LeventErkok]

This QuickCheck bug seems relevant: nick8325/quickcheck#113

Most likely the failing machine has an older version of QuickCheck that exhibits this problem. Need to upgrade and see if the problem goes away.

[LeventErkok]

Indeed, the quick-check bug is the culprit here. Fixed via 442b15b by requiring a newer QuickCheck.

Looks like the bug was introduced either in QuickCheck 2.9 or 2.9.1. Version 2.8.1 doesn't have it, and 2.9.2 fixes it.