CVC4: Boogie crashes when using cvc4 with smt vectors

wrwg commented 3 years ago

Boogie crashes with:

Unhandled exception. System.AggregateException: One or more errors occurred. (Index was outside the bounds of the array.) (Index was outside the bounds of the array.)
 ---> System.IndexOutOfRangeException: Index was outside the bounds of the array.
   at Microsoft.Boogie.SMTLib.SMTLibProcess.ParseId() in /home/runner/work/boogie/boogie/Source/Provers/SMTLib/SMTLibProcess.cs:line 289
   at Microsoft.Boogie.SMTLib.SMTLibProcess.ParseSExprs(Boolean top)+MoveNext() in /home/runner/work/boogie/boogie/Source/Provers/SMTLib/SMTLibProcess.cs:line 389
   at System.Collections.Generic.LargeArrayBuilder`1.AddRange(IEnumerable`1 items)
   at System.Collections.Generic.EnumerableHelpers.ToArray[T](IEnumerable`1 source)
   at System.Linq.Enumerable.ToArray[TSource](IEnumerable`1 source)
   at Microsoft.Boogie.SMTLib.SMTLibProcess.ParseSExprs(Boolean top)+MoveNext() in /home/runner/work/boogie/boogie/Source/Provers/SMTLib/SMTLibProcess.cs:line 370

This is apparently model output produced by cvc4 while using smt arrays. This case works fine if using Boogie arrays instead.

Repro:

boogie -doModSetAnalysis -printVerifiedProceduresCount:0 -printModel:1 -enhancedErrorMessages:1 -monomorphize -proverOpt:SOLVER=cvc4 -proverOpt:PROVER_PATH=/home/wrwg/bin/cvc4 -useArrayTheory /proverOpt:O:smt.array.extensional=false -vcsCores:12 output.bpl

bug.zip

@barrettcw

wrwg commented 3 years ago

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

wrwg commented 3 years ago

Close wrong issue, this one is still active.

boogie-org / boogie

CVC4: Boogie crashes when using cvc4 with smt vectors #391