Unhandled Exception

Feb 17, 2016 at 2:31 PM
Edited Feb 17, 2016 at 2:41 PM
I am getting this error while applying corral to my code (the code is in boogie). I don't know internals of Corral. So I don't understand the reason behind this. Can anyone figure out the reason?
Here is the command that I used: corral the-module.ko.bpl /tryCTrace /noTraceOnDisk /printDataValues:1 /k:1 /useProverEvaluate /timeLimit:1200 /cex:1 /maxStaticLoopBound:1 /recursionBound:1
Thanks.
Trace:
Unhandled Exception:
System.ArgumentNullException: Argument cannot be null.
Parameter name: other
  at System.Collections.Generic.HashSet`1[System.String].IsSubsetOf (IEnumerable`1 other) [0x00000] in <filename unknown>:0 
  at cba.Util.RemoveVarsFromAttributes.Remove (Microsoft.Boogie.QKeyValue attr, System.Collections.Generic.HashSet`1 vars) [0x00000] in <filename unknown>:0 
  at cba.Util.RemoveVarsFromAttributes.VisitVariable (Microsoft.Boogie.Variable node) [0x00000] in <filename unknown>:0 
  at cba.Util.FixedVisitor.VisitIdentifierExpr (Microsoft.Boogie.IdentifierExpr node) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.IdentifierExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.VisitExpr (Microsoft.Boogie.Expr node) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.VisitExprSeq (IList`1 exprSeq) [0x00000] in <filename unknown>:0                                                                                
  at Microsoft.Boogie.StandardVisitor.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) [0x00000] in <filename unknown>:0                                                                
  at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) [0x00000] in <filename unknown>:0                                                               
  at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) [0x00000] in <filename unknown>:0                                                                            
  at Microsoft.Boogie.StandardVisitor.VisitExpr (Microsoft.Boogie.Expr node) [0x00000] in <filename unknown>:0                                                                        
  at Microsoft.Boogie.StandardVisitor.VisitAxiom (Microsoft.Boogie.Axiom node) [0x00000] in <filename unknown>:0                                                                      
  at Microsoft.Boogie.Axiom.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) [0x00000] in <filename unknown>:0                                                                  
  at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) [0x00000] in <filename unknown>:0                                                                            
  at Microsoft.Boogie.StandardVisitor.VisitDeclarationList (System.Collections.Generic.List`1 declarationList) [0x00000] in <filename unknown>:0                                      
  at Microsoft.Boogie.StandardVisitor.VisitProgram (Microsoft.Boogie.Program node) [0x00000] in <filename unknown>:0                                                                  
  at cba.Util.RemoveVarsFromAttributes.Prune (Microsoft.Boogie.Program program) [0x00000] in <filename unknown>:0                                                                     
  at cba.VariableSlicing.VisitProgram (Microsoft.Boogie.Program node) [0x00000] in <filename unknown>:0                                                                               
  at cba.VariableSlicePass.runCBAPass (cba.CBAProgram p) [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.Driver.run (System.String[] args) [0x00000] in <filename unknown>:0 
  at cba.Driver.Main (System.String[] args) [0x00000] in <filename unknown>:0 
[ERROR] FATAL UNHANDLED EXCEPTION: System.ArgumentNullException: Argument cannot be null.
Parameter name: other
  at System.Collections.Generic.HashSet`1[System.String].IsSubsetOf (IEnumerable`1 other) [0x00000] in <filename unknown>:0 
  at cba.Util.RemoveVarsFromAttributes.Remove (Microsoft.Boogie.QKeyValue attr, System.Collections.Generic.HashSet`1 vars) [0x00000] in <filename unknown>:0 
  at cba.Util.RemoveVarsFromAttributes.VisitVariable (Microsoft.Boogie.Variable node) [0x00000] in <filename unknown>:0 
  at cba.Util.FixedVisitor.VisitIdentifierExpr (Microsoft.Boogie.IdentifierExpr node) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.IdentifierExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.VisitExpr (Microsoft.Boogie.Expr node) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.VisitExprSeq (IList`1 exprSeq) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.VisitExpr (Microsoft.Boogie.Expr node) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.VisitAxiom (Microsoft.Boogie.Axiom node) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.Axiom.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.VisitDeclarationList (System.Collections.Generic.List`1 declarationList) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.VisitProgram (Microsoft.Boogie.Program node) [0x00000] in <filename unknown>:0 
  at cba.Util.RemoveVarsFromAttributes.Prune (Microsoft.Boogie.Program program) [0x00000] in <filename unknown>:0 
  at cba.VariableSlicing.VisitProgram (Microsoft.Boogie.Program node) [0x00000] in <filename unknown>:0 
  at cba.VariableSlicePass.runCBAPass (cba.CBAProgram p) [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.Driver.run (System.String[] args) [0x00000] in <filename unknown>:0 
  at cba.Driver.Main (System.String[] args) [0x00000] in <filename unknown>:0
Feb 21, 2016 at 10:12 PM
Closing this thread as this is no longer a problem. I reinstalled corral and now it is working fine.
Marked as answer by deLta30 on 2/21/2016 at 3:12 PM