Using `cvc5` on Windows goes into an infinite loop

[RyanGlScott]

This simple SBV program that uses CVC5 works fine on Linux:

module Main (main) where

import Data.SBV

main :: IO ()
main = do
  res <- proveWith cvc5{verbose = True} $ \x -> x `shiftL` 2 .== 4 * (x::SWord8)
  print res

However, it goes into an infinite loop on Windows. Here is all the output that it produces before looping:

** Calling: cvc5 --lang smt --incremental --no-interactive --nl-cov
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[FAIL] (set-option :diagnostic-output-channel "stdout")

At this point, I have to kill the GHC process. I'm unclear if this is an SBV issue or a CVC5 one, but it does seem odd that SBV wouldn't catch the failure and proceed. In case it's relevant, I'm using SBV 9.2 and:

$ cvc5 --version
This is cvc5 version 1.0.4 [git tag 1.0.4 branch HEAD]
compiled with GCC version 10-posix 20220113
on Jan 31 2023 17:55:07

[RyanGlScott]

If I put the SMT2 interaction into its own file:

; diagnostic.smt2
(set-option :print-success true)
(set-option :global-declarations true)
(set-option :diagnostic-output-channel "stdout")

And then run cvc5 on this directly, it fails with a more informative error message:

$ cvc5 --lang smt --incremental --no-interactive --nl-cov diagnostic.smt2
success
success
(error "Error in option parsing: Cannot open file: `""stdout""': unknown reason")

The fact that it is trying to open a file named "stdout" leads me to think that cvc5/cvc5#8900 may be involved. (The fact that this fails on Windows and not on Linux may simply be due to the fact that Windows' filesystem doesn't permit " characters in file names.) Still, I'm surprised that SBV isn't able to catch this error.

[LeventErkok]

It is surprising we fail to catch that indeed. Alas, I don't have a Windows machine to try it on. Definitely needs debugging. I wonder if the cvc5 process dies before we get access to the output. To be honest, while "happy path" is tested on Windows, the failure paths are almost never tested on anything but a Mac.

If anyone has access to a windows machine and can do some debugging, it'd be much appreciated.

[RyanGlScott]

If anyone has access to a windows machine and can do some debugging, it'd be much appreciated.

I can help with this. Where should I start?

[LeventErkok]

Let's first try to figure out if CVC5 has to be involved. I'd start with creating a fake solver script:

$ cat a.sh
read
echo "(error \"Error in option parsing: Cannot open file: \`\"\"stdout\"\"': unknown reason\")"

You'll have to create the equivalent of that that works on Windows; like a .bat file I suppose. Or you can write it in any language at all. Read a line; ignore it, and print the message we see from CVC5. Then:

$ SBV_CVC5=`realpath ./a.sh` ghci
Loaded package environment from /Users/lerkok/.ghc/x86_64-darwin-9.4.4/environments/default
GHCi, version 9.4.4: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /Users/lerkok/GoogleDrive/dotfiles/home/ghci
Prelude> :m + Data.SBV
Prelude Data.SBV> proveWith cvc5{verbose=True} $ \x -> x.==(2::SWord8)
** Calling: /Users/lerkok/qq/a.sh --lang smt --incremental --no-interactive --nl-cov
[GOOD] ; Automatically generated by SBV. Do not edit.
*** Exception:
*** Data.SBV: Failed to initiate contact with the solver!
***
***   Sent    : (set-option :print-success true)
***   Expected: success
***   Received: (error "Error in option parsing: Cannot open file: `""stdout""': unknown reason")
***
*** Try running in debug mode for further information.

CallStack (from HasCallStack):
  error, called at ./Data/SBV/SMT/SMT.hs:929:62 in sbv-9.2.5-95da1044:Data.SBV.SMT.SMT

The above is on a Mac, and is the desired/expected behavior.

If this loops forever too on Windows, then we can start looking into SBV itself. If it works well, then I suppose CVC5 is somehow involved and we have to look at if it's crashing and leaving the handle open still. (I'm guessing the latter, but the above is a quick way to see it's not a pure "SBV on Windows" problem.

[LeventErkok]

@RyanGlScott Looks like CVC5 folks actually fixed the issue with the filenames; so if you're looking for a workaround, simply upgrading your CVC5 to their latest might do the trick.

I still would like to fix this issue from an SBV perspective, of course. So, please keep the ticket open in either case.

[RyanGlScott]

I wrote a Haskell program that does the same thing as your a.sh:

module Main where

main :: IO ()
main = do
  _ <- getLine
  putStrLn "(error \"Error in option parsing: Cannot open file: `\"\"stdout\"\"': unknown reason\")"

And then compiled it to a.exe. After configuring SBV_CVC5=realpath ./a.exe`, I see the following output from SBV, which does in fact terminate:

> :m + Data.SBV
> proveWith cvc5{verbose=True} $ \x -> x.==(2::SWord8)
** Calling: C:/Users/winferno/Documents/Hacking/Haskell/a.exe --lang smt --incremental --no-interactive --nl-cov
[GOOD] ; Automatically generated by SBV. Do not edit.
*** Exception:
*** Data.SBV: Failed to initiate contact with the solver!
***
***   Sent    : (set-option :print-success true)
***   Expected: success
***   Received: (error "Error in option parsing: Cannot open file: `""stdout""': unknown reason")
***
*** Try running in debug mode for further information.

CallStack (from HasCallStack):
  error, called at .\Data\SBV\SMT\SMT.hs:929:62 in sbv-9.2-ca0dbd7db168a4e7f2c575837f659a4f53b0c479:Data.SBV.SMT.SMT

[LeventErkok]

Ah, I think I see what's going on here. The good news is that this isn't a Windows or CVC5 issue. And here's how to replicate on any platform:

module Main where

import System.IO

main :: IO ()
main = do
  _ <- getLine
  putStrLn "success"
  hFlush stdout

  _ <- getLine
  putStrLn "success"
  hFlush stdout

  _ <- getLine
  putStrLn "success"
  hFlush stdout

  _ <- getLine
  hPutStrLn stderr "(error \"Error in option parsing: Cannot open file: `\"\"stdout\"\"': unknown reason\")"
  hFlush stdout

  _ <- getLine
  pure ()

Note that this program puts the error message to stderr, not stdout. One of the first things SBV does is to tell the solver to print everything to stdout; but if that line fails, the output is put on stderr, which SBV is not looking at, and hence waiting forever. Kind of funny that we're trying to avoid exactly this sort of problem by redirecting everything to stdout, but I failed to consider the case what happens if that command itself fails.

Shouldn't be too hard to fix, let me see what I can do..

[LeventErkok]

@RyanGlScott Just committed https://github.com/LeventErkok/sbv/commit/8b226c3dfae1820183dff5ef091af3e9049b5378, which should resolve this issue, I think. (It'll still fail of course, but won't hang and will print something useful to the user.)

Can you give this a try on your Windows machine to see how it goes?

[RyanGlScott]

Hm, I think there is still something not quite right. If I run the program in https://github.com/LeventErkok/sbv/issues/644#issue-1604017403 in GHCi using commit 8b226c3dfae1820183dff5ef091af3e9049b5378, then it still goes into an infinite loop:

$ ghci Bug.hs
Loaded package environment from C:\Users\winferno\Documents\Hacking\Haskell\sbv\.ghc.environment.x86_64-mingw32-9.2.7
GHCi, version 9.2.7: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from C:\Users\winferno\AppData\Roaming\ghc\ghci.conf
Ok, one module loaded.
> main
** Calling: cvc5 --lang smt --incremental --no-interactive --nl-cov
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[FAIL] (set-option :diagnostic-output-channel "stdout")
# Hangs here

Very strangely, however, if I first compile the program and then run the resulting executable, then it does terminate. However, it's far from instant, as it takes about five seconds to get unstuck:

$ ghc Bug.hs
Loaded package environment from C:\Users\winferno\Documents\Hacking\Haskell\sbv\.ghc.environment.x86_64-mingw32-9.2.7
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
Linking Bug.exe ...

$ time ./Bug.exe
** Calling: cvc5 --lang smt --incremental --no-interactive --nl-cov
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[FAIL] (set-option :diagnostic-output-channel "stdout")
Bug.exe:
*** Data.SBV: Unexpected non-success response from CVC5:
***
***    Sent      : (set-option :diagnostic-output-channel "stdout")
***    Expected  : success
***    Received  : (error "Error in option parsing: Cannot open file: `""stdout""': unknown reason")
***
***    Stdout    : fd:4: hGetContents: illegal operation (handle is semi-closed)
***    Stderr    : fd:5: hGetContents: illegal operation (handle is semi-closed)
***    Exit code : ExitFailure 1
***    Executable: C:\Users\winferno\Software\what4-solvers\cvc5.exe
***    Options   : --lang smt --incremental --no-interactive --nl-cov
***
***    Reason    : Backend solver reports it does not support this option.
***                Check the spelling, and if correct please report this as a
***                bug/feature request with the solver!

real    0m5.182s
user    0m0.000s
sys     0m0.000s

I'm not quite sure what to make of this.

[LeventErkok]

@RyanGlScott I had another go to clean-up the code, there was some extra blocking.

Note that SBV always does a 5-second wait in case something goes wrong. This allows the solver to spit out as much as it can, so we can grab it from stdout/stderr and not kill the process prematurely. Perhaps this wait is way too long. But since this should be a rare occurrence (assuming there are no bugs), perhaps it's not too terrible.

So, do expect a wait at the end for a little bit. But I'm hoping https://github.com/LeventErkok/sbv/commit/ba7178eb7baa63e144eb56c9b2e50d537163f89d will work as expected. Can you give that a try?

[RyanGlScott]

Note that SBV always does a 5-second wait in case something goes wrong.

Ah, my mistake!

But I'm hoping ba7178eb7baa63e144eb56c9b2e50d537163f89d will work as expected. Can you give that a try?

I'm afraid it's still not working. In fact, as of commit ba7178eb7baa63e144eb56c9b2e50d537163f89d, the program hangs in both GHCi and in a compiled executable.

[LeventErkok]

Bummer.. Can you test it by faking cvc with the following program:

module Main where

import System.IO

main :: IO ()
main = do
  _ <- getLine
  putStrLn "success"
  hFlush stdout

  _ <- getLine
  putStrLn "success"
  hFlush stdout

  _ <- getLine
  hPutStrLn stderr "(error \"Error in option parsing: Cannot open file: `\"\"stdout\"\"': unknown reason\")"
  hFlush stdout

  _ <- getLine
  pure ()

On my Mac, it works with this "fake" solver. I'd like to know what the behavior is on Windows.

[RyanGlScott]

After setting export SBV_CVC5=`realpath ./FakeSolver.exe`, if I run the program, I get this followed by a hang:

$ ./Bug.exe
** Calling: C:/Users/winferno/Documents/Hacking/Haskell/sbv/examples/FakeSolver.exe --lang smt --incremental --no-interactive --n
l-cov
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :diagnostic-output-channel "stdout")

At this point, I have to kill the process to make it stop. A similar hang happens in GHCi, except that I am able to Ctrl-C it successfully after the hang.

[LeventErkok]

Just to make sure I'm not imagining things, if you could try the same experiment on a Linux/Mac machine, that'd be great. That way we can focus on this being a Windows only problem.

If that's the case (i.e., if you also get it working fine on Mac/Linux), then I'd suspect something fishy is going on with:

https://github.com/LeventErkok/sbv/blob/ba7178eb7baa63e144eb56c9b2e50d537163f89d/Data/SBV/SMT/SMT.hs#L769

when run on Windows. We will need to put a print statement around there to see what's going on I guess. If you can experiment with that, it'd be really nice. Otherwise, I'll need to figure out how to acquire a windows machine to debug, perhaps you have one that can grant me remote access somehow?

[RyanGlScott]

Indeed, I can confirm that the fake solver does in fact terminate on Linux:

$ ./Bug 
** Calling: /home/rscott/Documents/Hacking/Haskell/sbv/examples/FakeSolver --lang smt --incremental --no-interactive --nl-cov
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[FAIL] (set-option :produce-models true)
Bug: 
*** Data.SBV: Unexpected non-success response from CVC5:
***
***    Sent      : (set-option :produce-models true)
***    Expected  : success
***    Received  : (error "Error in option parsing: Cannot open file: `""stdout""': unknown reason")
***
***    Exit code : ExitFailure (-15)
***    Executable: /home/rscott/Documents/Hacking/Haskell/sbv/examples/FakeSolver
***    Options   : --lang smt --incremental --no-interactive --nl-cov
***
***    Reason    : Backend solver reports it does not support this option.
***                Check the spelling, and if correct please report this as a
***                bug/feature request with the solver!

I'll add some debug printing around the call to hReady in coll.

[LeventErkok]

Great! So, this is a Windows problem only, and has really nothing to do with CVC5.

Could have something to do with buffering, we might have to explicitly set buffering options. I thought the Posix layer made programs work in exactly the same way on different OSs, but I suppose that's not true.

Note that, at this point, it should also be possible to create a failing test case that has nothing to do with SBV. Establish a pipe, and do a timeout based read from a channel that the corresponding process writes something to. (Or along those lines.) This way it might be easier to debug, and also report to GHC folks if it ends up being something they need to take a look at.

[RyanGlScott]

Your mention of POSIX made me remember that GHC on Windows actually has two IO managers: there is --io-manager=posix (which is what GHC uses by default), and --io-manager=native. I decided to see what would happen when I run the original program with --io-manager=native, and lo and behold, it behaves as you would expect:

$ ./Bug.exe +RTS --io-manager=native -RTS
** Calling: cvc5 --lang smt --incremental --no-interactive --nl-cov
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[FAIL] (set-option :diagnostic-output-channel "stdout")
Bug.exe:
*** Data.SBV: Unexpected non-success response from CVC5:
***
***    Sent      : (set-option :diagnostic-output-channel "stdout")
***    Expected  : success
***    Received  : (error "Error in option parsing: Cannot open file: `""stdout""': unknown reason")
***
***    Exit code : ExitFailure 1
***    Executable: C:\Users\winferno\Software\what4-solvers\cvc5.exe
***    Options   : --lang smt --incremental --no-interactive --nl-cov
***
***    Reason    : Backend solver reports it does not support this option.
***                Check the spelling, and if correct please report this as a
***                bug/feature request with the solver!

And with FakeSolver.exe:

$ export SBV_CVC5=`realpath ./FakeSolver.exe`
$ ./Bug.exe +RTS --io-manager=native -RTS
** Calling: C:/Users/winferno/Documents/Hacking/Haskell/sbv/examples/FakeSolver.exe --lang smt --incremental --no-interactive --nl-cov
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
Bug.exe:
*** Data.SBV: hwnd:0x00000000000001f0: hGetLine: invalid argument (The operation completed successfully.):
***
***    Sent      : (set-option :produce-models true)
***
***    Executable: C:\Users\winferno\Documents\Hacking\Haskell\sbv\examples\FakeSolver.exe
***    Options   : --lang smt --incremental --no-interactive --nl-cov

(That output is rather weird, but one problem at a time.)

So the bug is about --io-manager=posix in particular. With that in mind, I added some debug printing around hReady:

diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs
index 4c109d05..f98bc8e7 100644
--- a/Data/SBV/SMT/SMT.hs
+++ b/Data/SBV/SMT/SMT.hs
@@ -766,7 +766,16 @@ runSolver cfg ctx execPath opts pgm continuation

                                              -- Carefully grab things as they are ready. But don't block!
                                              collectH handle = reverse <$> coll ""
-                                               where coll sofar = do b <- hReady handle
+                                               where coll sofar = do putStrLn $ unlines
+                                                                       [ "RGS coll 1"
+                                                                       , show handle
+                                                                       , sofar
+                                                                       ]
+                                                                     b <- hReady handle
+                                                                     putStrLn $ unlines
+                                                                       [ "RGS coll 2"
+                                                                       , show b
+                                                                       ]
                                                                      if b
                                                                         then hGetChar handle >>= \c -> coll (c:sofar)
                                                                         else pure sofar

And here is what I get when running with --io-manager=posix:

$ ./Bug.exe +RTS --io-manager=posix -RTS
** Calling: C:/Users/winferno/Documents/Hacking/Haskell/sbv/examples/FakeSolver.exe --lang smt --incremental --no-interactive --nl-cov
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
RGS coll 1
{handle: fd:4}

At which point the program hangs. I get the same output regardless of whether I use the real cvc5 or FakeSolver.exe. (For comparison, running with --io-manager=native doesn't print any debug output at all.) So if I'm reading that correctly, hReady is blocking for some reason, which definitely feels like a bug.

[LeventErkok]

Great sleuthing! At this point, your knowledge of this problem is beyond mine.. I'll assign this ticket to you and feel free to submit a PR if anything needs to change on the SBV side.. Thanks!

[RyanGlScott]

Do you think you could help me distill down a small, channel-based example (like the one you refer to in https://github.com/LeventErkok/sbv/issues/644#issuecomment-1454294276) that does the same inter-process communication that SBV does? I could try to do this myself, but since I am not familiar with the code in SBV, it would probably take me much longer to minimize the issue.

[LeventErkok]

Sure.. I'll give it a shot; sometime next week I hope.

[RyanGlScott]

Thanks!

[LeventErkok]

Maybe something like this?

$ cat Producer.hs
module Main where

import System.IO

main :: IO ()
main = do
   s <- getLine
   putStrLn $ "Responding to: " ++ s
   hFlush stdout

   _ <- getLine
   pure ()
$ cat Consumer.hs
module Main (main) where

import Control.Concurrent
import System.Environment
import System.Process
import System.IO

main :: IO ()
main = do
  args <- getArgs
  pgm  <- case args of
            [p] -> pure p
            _   -> error "Pass the path to the producer executable"
  (inp, out, _, _) <- runInteractiveProcess pgm [] Nothing Nothing

  hPutStrLn inp "Hello"
  hFlush inp
  threadDelay 1000000

  let collect = reverse <$> go ""
      go sofar = do isReady <- hReady out
                    if isReady
                       then do c <- hGetChar out
                               go (c : sofar)
                       else pure sofar

  s <- collect
  putStrLn $ "Producer says: " ++ s
$ cat test
ghc -o Producer Producer.hs
ghc -o Consumer Consumer.hs
./Consumer ./Producer

Then:

$ ./test
Producer says: Responding to: Hello

I wonder how this behaves on Windows with both io-managers. If the native one terminates but posix doesn't, I think you'd have a smoking gun.

[RyanGlScott]

Thanks for the minimal example! --io-manager=posix does in fact terminate on this example:

$ ghc-9.2.7 -fforce-recomp Producer.hs -rtsopts
$ ghc-9.2.7 -fforce-recomp Consumer.hs -rtsopts
$ ./Consumer.exe ./Producer.exe +RTS --io-manager=posix -RTS
Producer says: Responding to: Hello

(I used GHC 9.2.7 above, but I get the same results with 9.4.4 and 9.6.1-alpha3 as well.)

That being said, --io-manager=native actually behaves differently here:

$ ./Consumer.exe ./Producer.exe +RTS --io-manager=native -RTS
Producer says:

That's not a hang: it just prints out "Producer says:" and terminates. I've opened GHC#23069 for this particular issue. I'm unclear if this issue is related to any of the oddities observed above, however (either the hang or the hGetLine: invalid argument (The operation completed successfully.) quirk).

[LeventErkok]

It is bizarre indeed. I'm not sure if the cure to this will cure SBV; whose communication is a bit more involved. (It uses both stdout and stderr, maybe that plays a role. Also a call to timeout..)

But let's see what the GHC guys have to say about this; perhaps whatever they propose can be adopted to SBV.

[RyanGlScott]

The cvc5-1.0.5 release includes a fix for cvc5/cvc5#8900, and I am now able to run cvc5 directly on the program in https://github.com/LeventErkok/sbv/issues/644#issuecomment-1449143358 without issues. Unfortunately, SBV itself still doesn't play nicely with cvc5-1.0.5. If I run the SBV program in https://github.com/LeventErkok/sbv/issues/644#issue-1604017403 with cvc5-1.0.5 and --io-manager=posix, then it hangs in a different spot:

$ PATH=$USERPROFILE/Desktop:$PATH ./Bug.exe +RTS --io-manager=posix -RTS
** Calling: cvc5 --lang smt --incremental --no-interactive --nl-cov
[GOOD] ; Automatically generated by SBV. Do not edit.
# Hangs

And --io-manager=native once again gives a mysterious hGetLine: invalid argument (The operation completed successfully.) error:

./Bug.exe +RTS --io-manager=native -RTS
** Calling: cvc5 --lang smt --incremental --no-interactive --nl-cov
[GOOD] ; Automatically generated by SBV. Do not edit.
Bug.exe:
*** Data.SBV: hwnd:0x00000000000001f0: hGetLine: invalid argument (The operation completed successfully.):
***
***    Sent      : (set-option :print-success true)
***
***    Executable: C:\Users\winferno\Desktop\cvc5.exe
***    Options   : --lang smt --incremental --no-interactive --nl-cov

The latter in particular is quite strange. I wonder if I can reproduce this independently of SBV by spawning a cvc5-1.0.5 subprocess via runInteractiveProcess...

[LeventErkok]

Oh, this sounds real bad.. Definitely needs debugging!

[RyanGlScott]

Interestingly, removing the use of the --no-interactive option when invoking cvc5 as a subprocess avoids the issue:

diff --git a/Data/SBV/Provers/CVC5.hs b/Data/SBV/Provers/CVC5.hs
index c26af933..759e053c 100644
--- a/Data/SBV/Provers/CVC5.hs
+++ b/Data/SBV/Provers/CVC5.hs
@@ -28,7 +28,7 @@ cvc5 = SMTSolver {
            name         = CVC5
          , executable   = "cvc5"
          , preprocess   = clean
-         , options      = const ["--lang", "smt", "--incremental", "--no-interactive", "--nl-cov"]
+         , options      = const ["--lang", "smt", "--incremental", {-"--no-interactive",-} "--nl-cov"]
          , engine       = standardEngine "SBV_CVC5" "SBV_CVC5_OPTIONS"
          , capabilities = SolverCapabilities {
                                 supportsQuantifiers        = True

[LeventErkok]

Interesting. Does it actually work without that setting? If memory serves, without that setting cvc printed a lot of headers and stuff. That’d certainly throw SBV off, I think. Doesn’t it?

[RyanGlScott]

Does it actually work without that setting?

I ran all of the SBV test cases that mention cvc5, and as far as I can tell, they all pass without the use of --no-interactive... well, all except nonlinear_cvc4. (Despite its name, it actually uses cvc5, not cvc4.) Regardless of whether or not I pass --no-interactive, that test segfaults for me on Windows. I've opened cvc5/cvc5#9567 upstream for this.

If memory serves, without that setting cvc printed a lot of headers and stuff.

I didn't see this when testing cvc5, but I think this could be the case for cvc4. I was able to find a single test case in the SBV test suite that uses cvc4 (query_cvc4), and if I run it without --no-interactive-prompt (the cvc4 counterpart to cvc5's --no-interactive), then the test fails with:

SBV
  Basics.QueryIndividual
    query_cvc4: FAIL (0.06s)

      *** Data.SBV: Failed to initiate contact with the solver!
      ***
      ***   Sent    : (set-option :print-success true)
      ***   Expected: success
      ***   Received: cvc4 1.8 assertions:off
      ***
      *** Try running in debug mode for further information.

      CallStack (from HasCallStack):
        error, called at .\Data\SBV\SMT\SMT.hs:956:62 in sbv-9.2.5-inplace:Data.SBV.SMT.SMT

1 out of 1 tests failed (1.84s)

Very strangely, this doesn't happen if I run the same cvc4 command locally, regardless of whether or not I pass --no-interactive-prompt. Perhaps cvc4 only prints this cvc4 1.8 assertions:off message if its input/output are redirected through a pipe? In any case, it's not that big of a deal, since it only appears to affect cvc4 (which doesn't suffer from this infinite loop issue in the first place).

[LeventErkok]

Fantastic! Great sleuthing. And I was able to get a clean test-suite run on my Mac after removing the --no-interactive parameter. I still want to check with the CVC5 folks that this is within their expectations.

Everything is committed to SBV head, if you want to do some testing with that.

[RyanGlScott]

Great! I am now able to run all of the SBV test cases involving cvc5 (with the exception of nonlinear_cvc5). I suppose there is still the underlying issue of whether GHC is behaving as expected when invoking runInteractiveProcess "cvc5" ["--no-interactive", ...], but I'll await feedback on https://github.com/cvc5/cvc5/issues/8900#issuecomment-1468637539 before investing further effort into investigating that.

[LeventErkok]

Awesome. I think we can close this ticket now though? I don't think there's much left for SBV to do regarding this problem.