Failing to initiate contact with cvc4

[MrChico]

Hi and thanks for a great package!

All seems to work well for me with z3, but when trying cvc4, I'm unable to connect to the solver. It seems the messages sent from sbv are also being interpreted as the response from cvc4. Here is the transcript generated when starting runSMTWith cvc4{transcript="cvc4log"}:

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; SBV: Starting at 2020-04-08 19:45:26.533425 CEST
;;;
;;;           Solver    : CVC4
;;;           Executable: /nix/store/jsnfli5xswz8qhkbc2bah8ib5ldr1j60-cvc4-1.6/bin/cvc4
;;;           Options   : --lang smt --incremental --interactive --no-interactive-prompt
;;;
;;; This file is an auto-generated loadable SMT-Lib file.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; [19:45:26.542] [Timeout: 5s] Sending:
(set-option :print-success true)
; [19:45:26.621] Received: (set-option :print-success true)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; SBV: Caught an exception at 2020-04-08 19:45:26.622487 CEST
;;;
;;;   *** Data.SBV: Failed to initiate contact with the solver!
;;;   ***
;;;   ***   Sent    : (set-option :print-success true)
;;;   ***   Expected: success
;;;   ***   Received: (set-option :print-success true)
;;;   ***
;;;   *** Try running in debug mode for further information.
;;;
;;;   CallStack (from HasCallStack):
;;;     error, called at ./Data/SBV/SMT/SMT.hs:844:62 in sbv-8.4-KqHl8MVtDy9wIfdO9hYfz:Data.SBV.SMT.SMT
;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; SBV: Finished at 2020-04-08 19:45:26.622813 CEST
;;;
;;; Exit code: ExitFailure (-6)
;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

I've tried sending the same request manually to cvc4 and it seems to return success as expected. Any idea what might be going on?

[LeventErkok]

I cannot reproduce this:

Prelude Data.SBV> proveWith cvc4{verbose=True} $ \x -> x + x .== 2 * (x::SWord8)
** Calling: cvc4 --lang smt --incremental --interactive --no-interactive-prompt --model-witness-choice
[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")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic QF_BV)
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s2 () (_ BitVec 8) #x02)
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () (_ BitVec 8))
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s1 () (_ BitVec 8) (bvadd s0 s0))
[GOOD] (define-fun s3 () (_ BitVec 8) (bvmul s0 s2))
[GOOD] (define-fun s4 () Bool (= s1 s3))
[GOOD] (assert (not s4))
[SEND] (check-sat)
[RECV] unsat
*** Solver   : CVC4
*** Exit code: ExitSuccess
*** Std-out  :
Q.E.D.

Here's my CVC4 version:

$ cvc4 -V
This is CVC4 version 1.8-prerelease [git master c9fd28a3]
compiled with GCC version 4.2.1 Compatible Apple LLVM 11.0.3 (clang-1103.0.32.29)
on Mar 26 2020 12:10:53

Looks like you're using a bit of an older one. Can you try upgrading your CVC4 and see if the problem goes away?

[MrChico]

Yup, upgraded to 1.7 and it seems to work better. Thanks!

[LeventErkok]

Glad to hear!