1
Vote

[Duality] ``Prover error: unknown predicate from prover: q@fp``

description

When trying to use duality on the following program
https://github.com/smackers/sbb/blob/master/sv-comp/floats-cdfpl/newton_1_1_true-unreach-call.i_.bpl
like so...
corral.exe sv-comp/floats-cdfpl/newton_1_1_true-unreach-call.i_.bpl /useDuality
Z3 (I'm using Z3 4.3.2) emits a prover error then corral crashes
Warning: Using default recursion bound of 1
Single threaded program detected
Verifying program while tracking: {assertsPassed}
generate: 0.0557s
Verifying main_SeqInstr...
Prover error: unknown predicate from prover: q@fp

Unhandled Exception:
System.NullReferenceException: Object reference not set to an instance of an object
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.CheckRPFP (System.String descriptiveName, Microsoft.Boogie.RPFP _rpfp, Microsoft.Boogie.ErrorHandler handler, Microsoft.Boogie.Node& cex, System.Collections.Generic.Dictionary`2 varSubst, System.Collections.Generic.Dictionary`2 extra_bound) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.FixedpointVC.Check (Microsoft.Boogie.Node& cexroot) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.FixedpointVC.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback collector) [0x00000] in <filename unknown>:0 
  at VC.ConditionGeneration.VerifyImplementation (Microsoft.Boogie.Implementation impl, System.Collections.Generic.List`1& errors, System.String requestId) [0x00000] in <filename unknown>:0 
  at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, Boolean needErrorTraces, System.Collections.Generic.List`1& allErrors, System.Collections.Generic.List`1& timedOut, Boolean isCBA) [0x00000] in <filename unknown>:0 
  at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, System.Collections.Generic.List`1& allErrors, Boolean isCBA) [0x00000] in <filename unknown>:0 
  at cba.VerificationPass.feedToBoogie (cba.CBAProgram p) [0x00000] in <filename unknown>:0 
  at cba.VerificationPass.runCBAPass (cba.CBAProgram prog) [0x00000] in <filename unknown>:0 
  at cba.CompilerPass.runPass (Microsoft.Boogie.Program inp) [0x00000] in <filename unknown>:0 
  at ProgTransformation.TransformationPass.run (ProgTransformation.PersistentProgram inp) [0x00000] in <filename unknown>:0 
  at cba.CompilerPass.run (cba.PersistentCBAProgram inp) [0x00000] in <filename unknown>:0 
  at cba.CBADriver.VerifyProgram (cba.PersistentCBAProgram& prog, cba.VarSet trackedVars, Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x00000] in <filename unknown>:0 
  at cba.CBADriver.checkProgram (cba.PersistentCBAProgram& prog, cba.VarSet trackedVars, Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x00000] in <filename unknown>:0 
[ERROR] FATAL UNHANDLED EXCEPTION: System.NullReferenceException: Object reference not set to an instance of an object
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.CheckRPFP (System.String descriptiveName, Microsoft.Boogie.RPFP _rpfp, Microsoft.Boogie.ErrorHandler handler, Microsoft.Boogie.Node& cex, System.Collections.Generic.Dictionary`2 varSubst, System.Collections.Generic.Dictionary`2 extra_bound) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.FixedpointVC.Check (Microsoft.Boogie.Node& cexroot) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.FixedpointVC.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback collector) [0x00000] in <filename unknown>:0 
  at VC.ConditionGeneration.VerifyImplementation (Microsoft.Boogie.Implementation impl, System.Collections.Generic.List`1& errors, System.String requestId) [0x00000] in <filename unknown>:0 
  at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, Boolean needErrorTraces, System.Collections.Generic.List`1& allErrors, System.Collections.Generic.List`1& timedOut, Boolean isCBA) [0x00000] in <filename unknown>:0 
  at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, System.Collections.Generic.List`1& allErrors, Boolean isCBA) [0x00000] in <filename unknown>:0 
  at cba.VerificationPass.feedToBoogie (cba.CBAProgram p) [0x00000] in <filename unknown>:0 
  at cba.VerificationPass.runCBAPass (cba.CBAProgram prog) [0x00000] in <filename unknown>:0 
  at cba.CompilerPass.runPass (Microsoft.Boogie.Program inp) [0x00000] in <filename unknown>:0 
  at ProgTransformation.TransformationPass.run (ProgTransformation.PersistentProgram inp) [0x00000] in <filename unknown>:0 
  at cba.CompilerPass.run (cba.PersistentCBAProgram inp) [0x00000] in <filename unknown>:0 
  at cba.CBADriver.VerifyProgram (cba.PersistentCBAProgram& prog, cba.VarSet trackedVars, Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x00000] in <filename unknown>:0 
  at cba.CBADriver.checkProgram (cba.PersistentCBAProgram& prog, cba.VarSet trackedVars, Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x00000] in <filename unknown>:0 

comments