CVC4: non-terminating verification problem + Boogie SMTlib output not recognized

[wrwg]

The attached Boogie file when run with cvc4 leads to non-termination with rapid memory growth. It's unclear whether this is caused by cvc4 or by Boogie (or both).

Trying to isolate the problem by using the SMT output Boogie generates and feed it directly into cvc4 did not work because cvc4 rejects this output with (error "Cannot push when not solving incrementally (use --incremental)"). (An independent bug.)

Repro (careful you may need to interrupt it can freeze your machine):

boogie -doModSetAnalysis -printVerifiedProceduresCount:0 -printModel:1 -enhancedErrorMessages:1 -monomorphize -proverOpt:SOLVER=cvc4 -proverOpt:PROVER_PATH=/home/wrwg/bin/cvc4 -proverOpt:O:smt.QI.EAGER_THRESHOLD=100 -proverOpt:O:smt.QI.LAZY_THRESHOLD=100 -vcsCores:12 -proverLog:@PROC@.smt output.bpl

To reproduce the smtlib problem, take the generated .smt file and pass it to cvc4.

@barrettcw

bug.zip

[barrettcw]

The error message from cvc4 is not a bug, it's a feature. cvc4 does not by default accept push and pop commands (because in general it is worse for performance to enable this feature). Just pass the -i flag (short for --incremental) and it should work fine.

[wrwg]

The error message from cvc4 is not a bug, it's a feature. cvc4 does not by default accept push and pop commands (because in general it is worse for performance to enable this feature). Just pass the -i flag (short for --incremental) and it should work fine.

Great with that input I could nail the issue down to cvc4. Now I have the smtlib file which lets cvc4 quickly grow to gigabytes. Should I file an issue on cvc4 github or how do I report?

[barrettcw]

Yes! Please file an issue on cvc4's github issue tracker.

[wrwg]

Opened https://github.com/CVC4/CVC4/issues/6495 and closing this one.