search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
240 stars 33 forks source link

CVC5 solver creates a file called "stdout" #620

Closed Torrencem closed 2 years ago

Torrencem commented 2 years ago

When using the CVC5 solver, a file called "stdout" is created in the pwd, even if redirectVerbose=None. This might be a change from CVC4.

619

Torrencem commented 2 years ago

The attached PR fixes this

LeventErkok commented 2 years ago

I believe this is already fixed in CVC5, see here: https://github.com/cvc5/cvc5/issues/7478

Perhaps you need a newer version of CVC5?

Torrencem commented 2 years ago

You're right, thanks