Crash with "Must find a successor" exception

[zvonimir]

Corral crashes on the attached file mul-sim4.txt with the exception I inlined below. I am using the latest commit of Corral (1513113) and Z3 release 4.5.0.

CoreLib.InsufficientDetailsToConstructCexPath: StratifiedInliningErrorReporter: Must find a successor
  at CoreLib.StratifiedInliningErrorReporter.GetAbsyTraceLabels (VC.StratifiedVC svc, System.Collections.Generic.IList`1[T] labels) [0x0009c] in <8dc37349d776400598537372a737c18f>:0
  at CoreLib.StratifiedInliningErrorReporter.GetAbsyTrace (VC.StratifiedVC svc, System.Collections.Generic.IList`1[T] labels) [0x00020] in <8dc37349d776400598537372a737c18f>:0
  at CoreLib.StratifiedInliningErrorReporter.OnModel (System.Collections.Generic.IList`1[T] labels, Microsoft.Boogie.Model model, Microsoft.Boogie.ProverInterface+Outcome proverOutcome) [0x0001e] in <8dc37349d776400598537372a737c18f>:0
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.CheckOutcomeCore (Microsoft.Boogie.ProverInterface+ErrorHandler handler, System.Int32 taskID) [0x005b8] in <e8f06521e414414b933e01187da2b2e2>:0
  at CoreLib.StratifiedInlining.CheckVC (Microsoft.Boogie.ProverInterface+ErrorHandler reporter) [0x0003c] in <8dc37349d776400598537372a737c18f>:0
  at CoreLib.StratifiedInlining.Fwd (System.Collections.Generic.HashSet`1[T] openCallSites, CoreLib.StratifiedInliningErrorReporter reporter, System.Boolean main, System.Int32 recBound) [0x000d7] in <8dc37349d776400598537372a737c18f>:0
  at CoreLib.StratifiedInlining.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) [0x00550] in <8dc37349d776400598537372a737c18f>:0
  at VC.ConditionGeneration.VerifyImplementation (Microsoft.Boogie.Implementation impl, System.Collections.Generic.List`1[Microsoft.Boogie.Counterexample]& errors, System.String requestId) [0x00017] in <c2ed7d03076b4445914f73a71961c2e3>:0
  at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, System.Boolean needErrorTraces, System.Collections.Generic.List`1[cba.Util.BoogieErrorTrace]& allErrors, System.Collections.Generic.List`1[System.String]& timedOut, System.Boolean isCBA) [0x00336] in <8dc37349d776400598537372a737c18f>:0
  at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, System.Collections.Generic.List`1[cba.Util.BoogieErrorTrace]& allErrors, System.Boolean isCBA) [0x00006] in <8dc37349d776400598537372a737c18f>:0
  at cba.VerificationPass.feedToBoogie (cba.CBAProgram p) [0x0004f] in <8dc37349d776400598537372a737c18f>:0
  at cba.VerificationPass.runCBAPass (cba.CBAProgram prog) [0x00019] in <8dc37349d776400598537372a737c18f>:0
  at cba.CompilerPass.runPass (Microsoft.Boogie.Program inp) [0x00007] in <8dc37349d776400598537372a737c18f>:0
  at ProgTransformation.TransformationPass.run (ProgTransformation.PersistentProgram inp) [0x00086] in <d3661e2e55744966b56b7768b842aad4>:0
  at cba.CompilerPass.run (cba.PersistentCBAProgram inp) [0x00006] in <8dc37349d776400598537372a737c18f>:0
  at cba.CBADriver.VerifyProgram (cba.PersistentCBAProgram& prog, cba.VarSet trackedVars, System.Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x0011a] in <c90727d97d374736b02486f43e6a8385>:0
  at cba.CBADriver.checkProgram (cba.PersistentCBAProgram& prog, cba.VarSet trackedVars, System.Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x00022] in <c90727d97d374736b02486f43e6a8385>:0
  at cba.Driver.checkAndRefine (cba.PersistentCBAProgram prog, cba.RefinementState refinementState, System.Action`2[T1,T2] printTrace, cba.ErrorTrace& cexTrace) [0x000de] in <c90727d97d374736b02486f43e6a8385>:0
  at cba.Driver.run (System.String[] args) [0x003f1] in <c90727d97d374736b02486f43e6a8385>:0
  at cba.Driver.Main (System.String[] args) [0x0005a] in <c90727d97d374736b02486f43e6a8385>:0
[ERROR] FATAL UNHANDLED EXCEPTION: CoreLib.InsufficientDetailsToConstructCexPath: StratifiedInliningErrorReporter: Must find a successor
  at CoreLib.StratifiedInliningErrorReporter.GetAbsyTraceLabels (VC.StratifiedVC svc, System.Collections.Generic.IList`1[T] labels) [0x0009c] in <8dc37349d776400598537372a737c18f>:0
  at CoreLib.StratifiedInliningErrorReporter.GetAbsyTrace (VC.StratifiedVC svc, System.Collections.Generic.IList`1[T] labels) [0x00020] in <8dc37349d776400598537372a737c18f>:0
  at CoreLib.StratifiedInliningErrorReporter.OnModel (System.Collections.Generic.IList`1[T] labels, Microsoft.Boogie.Model model, Microsoft.Boogie.ProverInterface+Outcome proverOutcome) [0x0001e] in <8dc37349d776400598537372a737c18f>:0
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.CheckOutcomeCore (Microsoft.Boogie.ProverInterface+ErrorHandler handler, System.Int32 taskID) [0x005b8] in <e8f06521e414414b933e01187da2b2e2>:0
  at CoreLib.StratifiedInlining.CheckVC (Microsoft.Boogie.ProverInterface+ErrorHandler reporter) [0x0003c] in <8dc37349d776400598537372a737c18f>:0
  at CoreLib.StratifiedInlining.Fwd (System.Collections.Generic.HashSet`1[T] openCallSites, CoreLib.StratifiedInliningErrorReporter reporter, System.Boolean main, System.Int32 recBound) [0x000d7] in <8dc37349d776400598537372a737c18f>:0
  at CoreLib.StratifiedInlining.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) [0x00550] in <8dc37349d776400598537372a737c18f>:0
  at VC.ConditionGeneration.VerifyImplementation (Microsoft.Boogie.Implementation impl, System.Collections.Generic.List`1[Microsoft.Boogie.Counterexample]& errors, System.String requestId) [0x00017] in <c2ed7d03076b4445914f73a71961c2e3>:0
  at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, System.Boolean needErrorTraces, System.Collections.Generic.List`1[cba.Util.BoogieErrorTrace]& allErrors, System.Collections.Generic.List`1[System.String]& timedOut, System.Boolean isCBA) [0x00336] in <8dc37349d776400598537372a737c18f>:0
  at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, System.Collections.Generic.List`1[cba.Util.BoogieErrorTrace]& allErrors, System.Boolean isCBA) [0x00006] in <8dc37349d776400598537372a737c18f>:0
  at cba.VerificationPass.feedToBoogie (cba.CBAProgram p) [0x0004f] in <8dc37349d776400598537372a737c18f>:0
  at cba.VerificationPass.runCBAPass (cba.CBAProgram prog) [0x00019] in <8dc37349d776400598537372a737c18f>:0
  at cba.CompilerPass.runPass (Microsoft.Boogie.Program inp) [0x00007] in <8dc37349d776400598537372a737c18f>:0
  at ProgTransformation.TransformationPass.run (ProgTransformation.PersistentProgram inp) [0x00086] in <d3661e2e55744966b56b7768b842aad4>:0
  at cba.CompilerPass.run (cba.PersistentCBAProgram inp) [0x00006] in <8dc37349d776400598537372a737c18f>:0
  at cba.CBADriver.VerifyProgram (cba.PersistentCBAProgram& prog, cba.VarSet trackedVars, System.Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x0011a] in <c90727d97d374736b02486f43e6a8385>:0
  at cba.CBADriver.checkProgram (cba.PersistentCBAProgram& prog, cba.VarSet trackedVars, System.Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x00022] in <c90727d97d374736b02486f43e6a8385>:0
  at cba.Driver.checkAndRefine (cba.PersistentCBAProgram prog, cba.RefinementState refinementState, System.Action`2[T1,T2] printTrace, cba.ErrorTrace& cexTrace) [0x000de] in <c90727d97d374736b02486f43e6a8385>:0
  at cba.Driver.run (System.String[] args) [0x003f1] in <c90727d97d374736b02486f43e6a8385>:0
  at cba.Driver.Main (System.String[] args) [0x0005a] in <c90727d97d374736b02486f43e6a8385>:0

[akashlal]

Can you tell me the command line that you used?

[zvonimir]

Simply corral mul-sim4.bpl.
Btw, I remember this being the typical exception when Z3 incompleteness is encountered. However, I looked at the prover log, and I did not see the usual incompleteness suspects (quantifiers, arrays, etc). Hence, I am not sure if that is indeed the root cause.

[akashlal]

Interestingly, corral with Z3 version 4.4.0 succeeds. With 4.5.0, I do get the crash. I passed the additional flag /proverLog:log. When I feed log to z3-4.5.0 it prints:

(:reason-unknown "smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))")

I believe corral isn't designed to handle such kind of incompleteness.

[zvonimir]

Thanks @akashlal. I will explore this further on the Z3 side.
Btw, this is just a suggestion, but maybe it would be possible to print out a "gentler" error message when Z3 incompleteness is encountered instead of crashing.

[michael-emmi]

Interestingly this problem persists with Z3 versions 4.6.0, 4.7.1, 4.8.1, 4.8.3, and 4.8.4.

With Z3 versions 4.8.5 and 4.8.6, Z3 seems to spin (forever?).

With Z3 version 4.8.7, Z3 complains about an unknown model_compress parameter.

% corral  /proverLog:prover.log ~/Desktop/mul-sim4.bpl
Corral program verifier version 0.1.0.0
Warning: Using default recursion bound of 1
Single threaded program detected
Verifying program while tracking: {assertsPassed}
Prover error: line 17 column 28: unknown parameter 'model_compress'
Legal parameters are:
  auto_config (bool) (default: true)
  debug_ref_count (bool) (default: false)
  dot_proof_file (string) (default: proof.dot)
  dump_models (bool) (default: false)
  memory_high_watermark (unsigned int) (default: 0)
  memory_max_alloc_count (unsigned int) (default: 0)
  memory_max_size (unsigned int) (default: 0)
  model (bool) (default: true)
  model_validate (bool) (default: false)
  proof (bool) (default: false)
  rlimit (unsigned int) (default: 0)
  smtlib2_compliant (bool) (default: false)
  stats (bool) (default: false)
  timeout (unsigned int) (default: 4294967295)
  trace (bool) (default: false)
  trace_file_name (string) (default: z3.log)
  type_check (bool) (default: true)
  unsat_core (bool) (default: false)
  verbose (unsigned int) (default: 0)
  warning (bool) (default: true)
  well_sorted_check (bool) (default: false)
Corral encountered a prover error. Giving up.

[michael-emmi]

This PR fixes the last issue.

[michael-emmi]

With that fix, Z3 4.8.7 behaves as 4.8.5 and 4.8.6, spinning (forever?).