Symbooglix.Solver.SolverErrorException

[sebastian-kunze]

I am translating Java code to Boogie code for symbolic execution and run into an issue when using arrays within nested single arity maps.

// ######################################
// #        HEAP & LOCAL VARIABLES      #
// ######################################
type Ref;

type Bool;

type BoolHeap = [Ref][Bool] bool;

var boolHeap : BoolHeap;

// ######################################    
// #              METHODS               #
// ######################################

var array : [int] Bool;

const array$size : int;
axiom array$size == 5;

procedure someFunction(this : Ref) returns ()
{
 var pos   : int;
 var field : Bool;
 var value : bool;

 pos   := 0;
 field := array[pos]
 value := boolHeap[this][field];

 if (value) {

 }
}

Executing this example throws the following Symbooglix.Solver.SolverErrorException:

Symbooglix.Solver.SolverErrorException: (error "line 3 column 50: Invalid function declaration: unknown sort '@Bool'")(error "line 5 column 39: Invalid function declaration: unknown sort '@Bool'")
  at Symbooglix.Solver.SimpleSMTLIBSolver.ComputeSatisfiability (Symbooglix.Solver.Query query) <0x44ccb10 + 0x003cb> in <filename unknown>:0 
  at Symbooglix.Solver.ConstraintIndependenceSolver.ComputeSatisfiability (Symbooglix.Solver.Query query) <0x44cb070 + 0x00347> in <filename unknown>:0 
  at Symbooglix.Solver.SimpleSolver.InternalComputeSatisfiability (Symbooglix.Solver.Query query) <0x44ca958 + 0x000db> in <filename unknown>:0 
  at Symbooglix.Solver.SimpleSolver.CheckSatisfiability (Symbooglix.Solver.Query query) <0x44ca8e8 + 0x00027> in <filename unknown>:0 
  at Symbooglix.Executor.LookAheadGotoFork (Microsoft.Boogie.GotoCmd c) <0x44c8998 + 0x0052c> in <filename unknown>:0 
  at Symbooglix.Executor.Handle (Microsoft.Boogie.GotoCmd c) <0x44c8900 + 0x0003b> in <filename unknown>:0 
  at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
  at System.Dynamic.UpdateDelegates.UpdateAndExecuteVoid2[T0,T1] (System.Runtime.CompilerServices.CallSite site, System.Dynamic.T0 arg0, System.Dynamic.T1 arg1) <0x41fdeb0 + 0x00425> in <filename unknown>:0 
  at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
  at Symbooglix.Executor.ExecuteInstruction () <0x41facf8 + 0x001a4> in <filename unknown>:0 
  at Symbooglix.Executor.InternalRun (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x2d8ed00 + 0x0048b> in <filename unknown>:0 
  at Symbooglix.Executor.Run (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x2d8e938 + 0x000c3> in <filename unknown>:0 
Exiting with EXCEPTION_RAISED

[delcypher]

@sebkunze Sorry I've been very busy with paper deadlines recently. I'm taking a look at this now.

[delcypher]

@sebkunze This is now fixed. Thanks for reporting this.