You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
During our CI runs, calls that involve SBV are dumping debug lines to the log, such as [ISSUE] (define-fun s832 () (_BitVec 28) (concat s732 s831) -- dumping SMT files and other large things. This is recent, and does not happen when calling solvers via W4. The [ISSUE] line shows up here: https://github.com/LeventErkok/sbv/blob/bbab5b9aa5ef63d393120cca2e93df3b703626a1/Data/SBV/SMT/SMT.hs#L864
We also see other debug commands such as [SEND] and [RECV]. Is there a way to quiet this noisiness?
The text was updated successfully, but these errors were encountered:
We haven't changed anything recently involving the way SBV is handled, so I'm not sure why this would only be showing up now. In any case, we are in fact always passing pcVerbose = True in cryptol-remote-api, which can cause SBV to print verbose output. Apropos of nothing, we should probably stick to Cryptol's default of pcVerbose = False for remote API purposes.
We should try to match Cryptol's default settings when invoking the remote API,
but the `pcVerbose` value (`True`) didn't match the defaults. Changing this to
`False` should fix#1378. There is a separate question of whether remote API
users should be able to change this default, but for the time being, let's at
least be consistent between Cryptol's settings and the remote API's settings.
We should try to match Cryptol's default settings when invoking the remote API,
but the `pcVerbose` value (`True`) didn't match the defaults. Changing this to
`False` should fix#1378. There is a separate question of whether remote API
users should be able to change this default, but for the time being, let's at
least be consistent between Cryptol's settings and the remote API's settings.
During our CI runs, calls that involve SBV are dumping debug lines to the log, such as
[ISSUE] (define-fun s832 () (_BitVec 28) (concat s732 s831)
-- dumping SMT files and other large things. This is recent, and does not happen when calling solvers via W4. The[ISSUE]
line shows up here: https://github.com/LeventErkok/sbv/blob/bbab5b9aa5ef63d393120cca2e93df3b703626a1/Data/SBV/SMT/SMT.hs#L864We also see other debug commands such as
[SEND]
and[RECV]
. Is there a way to quiet this noisiness?The text was updated successfully, but these errors were encountered: