Merge

18 files changed, 692 insertions, 1035 deletions

diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index f439c8d0..7c8c472d 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -8,6 +8,7 @@ open MethodUnifier
 open Modularizer

 open PipelineUtils

 open Options

+open TypeChecker

 open Resolver

 open PrintUtils

 open DafnyPrinter

@@ -76,8 +77,9 @@ let rec MethodAnalysisPrinter onlyForThese assertion comp =
   | [] -> ""     

 

 //  =========================================================================

-/// For a given constant "o" (which is an object, something like "gensym32"), 

-/// finds a path of field references from "this". 

+/// For a given constant "objRefName" (which is an object, something like 

+/// "gensym32"), finds a path of field references from "this" (e.g. something

+/// like "this.next.next"). 

 ///

 /// Implements a backtracking search over the heap entries to find that

 /// path.  It starts from the given object, and follows the backpointers

@@ -140,7 +142,7 @@ let GetHeapExpr prog mthd heapInst =
                           objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc

                       ) prepostExpr

 

-let IsUnmodOnly (comp,meth) expr = 

+let IsUnmodConcrOnly prog (comp,meth) expr = 

   let isConstr = IsConstructor meth

   let rec __IsUnmodOnly args expr = 

     let __IsUnmodOnlyLst elist = 

@@ -151,27 +153,30 @@ let IsUnmodOnly (comp,meth) expr =
     | BoxLiteral(_)

     | Star        

     | VarDeclExpr(_)

-    | ObjLiteral(_)                        -> true

-    | VarLiteral(id)                       -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false)

-    | IdLiteral("null")                    -> true

-    | IdLiteral(id)                        -> if isConstr then false else true  //TODO: tempporary implementation

-    | Dot(e, fldName)                      -> if isConstr then false else __IsUnmodOnlyLst [e]

-        // TODO: this is how it should really work

-        // let lhsType = InferType prog e

-        // let isMod = IsFieldModifiable lhsType fldName

-        // (not isMod) && __IsUnmodOnlyLst [e]

+    | ObjLiteral(_)                         -> true

+    | VarLiteral(id)                        -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false)

+    | IdLiteral("null") | IdLiteral("this") -> true

+    | IdLiteral(id)                         -> 

+        not (isConstr || IsAbstractField comp id)

+    | Dot(e, fldName)                       -> //if isConstr then false else __IsUnmodOnlyLst [e] 

+        if isConstr then

+          false

+        else

+          // assume it is unmodifiable, because it is a method, so just check if it's concrete

+          let lhsType = InferType prog comp e |> Utils.ExtractOptionMsg (sprintf "Inference failed for %s" (PrintExpr 0 e))

+          IsConcreteField lhsType fldName          

     | AssertExpr(e)

     | AssumeExpr(e)

     | SeqLength(e)

     | LCIntervalExpr(e)

-    | UnaryExpr(_,e)                       -> __IsUnmodOnlyLst [e]

+    | UnaryExpr(_,e)                        -> __IsUnmodOnlyLst [e]

     | SelectExpr(e1, e2)

-    | BinaryExpr(_,_,e1,e2)                -> __IsUnmodOnlyLst [e1; e2]

+    | BinaryExpr(_,_,e1,e2)                 -> __IsUnmodOnlyLst [e1; e2]

     | IteExpr(e3, e1, e2)         

-    | UpdateExpr(e1, e2, e3)               -> __IsUnmodOnlyLst [e1; e2; e3]

-    | SequenceExpr(exprs) | SetExpr(exprs) -> __IsUnmodOnlyLst exprs

-    | MethodCall(rcv,_,_,aparams)          -> __IsUnmodOnlyLst (rcv :: aparams)

-    | ForallExpr(vars,e)                   -> __IsUnmodOnly (args @ vars) e

+    | UpdateExpr(e1, e2, e3)                -> __IsUnmodOnlyLst [e1; e2; e3]

+    | SequenceExpr(exprs) | SetExpr(exprs)  -> __IsUnmodOnlyLst exprs

+    | MethodCall(rcv,_,_,aparams)           -> __IsUnmodOnlyLst (rcv :: aparams)

+    | ForallExpr(vars,e)                    -> __IsUnmodOnly (args @ vars) e

   (* --- function body starts here --- *)

   __IsUnmodOnly (GetMethodInArgs meth) expr

 

@@ -185,7 +190,7 @@ let AddUnif indent e v unifMap =
   }

 

 //TODO: unifications should probably by "Expr <--> Expr" instead of "Expr <--> Const"

-let rec GetUnifications indent (comp,meth) heapInst unifs expr =

+let rec GetUnifications prog indent (comp,meth) heapInst unifs expr =

   let idt = Indent indent

   // - first looks if the give expression talks only about method arguments (args)

   // - then it tries to evaluate it to a constant

@@ -196,7 +201,7 @@ let rec GetUnifications indent (comp,meth) heapInst unifs expr =
     else      

       let builder = new CascadingBuilder<_>(unifsAcc)

       builder {

-        let! argsOnly = IsUnmodOnly (comp,meth) e |> Utils.BoolToOption

+        let! argsOnly = IsUnmodConcrOnly prog (comp,meth) e |> Utils.BoolToOption

         let! v = try Some(Eval heapInst (fun _ -> true) e |> Expr2Const) with ex -> None

         return AddUnif indent e v unifsAcc

       }

@@ -207,7 +212,7 @@ let rec GetUnifications indent (comp,meth) heapInst unifs expr =
 /// Returns a map (Expr |--> Const) containing unifications

 /// found for the given method and heap/env/ctx

 //  =======================================================

-let GetUnificationsForMethod indent comp m heapInst =

+let GetUnificationsForMethod indent prog comp m heapInst =

   let idt = Indent indent

   let rec GetArgValueUnifications args = 

     match args with

@@ -217,26 +222,34 @@ let GetUnificationsForMethod indent comp m heapInst =
             GetArgValueUnifications rest |> AddUnif indent (VarLiteral(name)) c

         | None -> failwith ("couldn't find value for argument " + name)

     | [] -> Map.empty

-  let rec GetFldValueUnifications fldNames unifs = 

-    match fldNames with

-    | fldName :: rest -> 

-        heapInst.assignments |> List.fold (fun acc asgn ->  

-                                             match asgn with 

-                                             | FieldAssignment((obj,Var(vname,_)), fldVal) when obj.name = "this" && vname = fldName -> 

-                                                 try 

-                                                   let c = Expr2Const fldVal

-                                                   AddUnif indent (IdLiteral(fldName)) c acc

-                                                 with

-                                                 | _ -> acc

-                                             | _ -> acc

-                                          ) unifs

-                             |> GetFldValueUnifications rest 

-    | [] -> unifs

+  let rec GetFldValueUnifications unifs = 

+    heapInst.assignments |> List.fold (fun acc asgn ->  

+                                         match asgn with 

+                                         | FieldAssignment((obj,Var(vname,_)), fldVal) -> 

+                                             try 

+                                               let comp = obj.objType |> FindComponentForType prog |> Utils.ExtractOption

+                                               if IsConcreteField comp vname then

+                                                 let path = GetObjRefExpr obj.name heapInst |> Utils.ExtractOption

+                                                 let c = Expr2Const fldVal

+                                                 AddUnif indent (Dot(path, vname)) c acc

+                                               else

+                                                 acc

+                                             with

+                                             | ex -> 

+                                                 Logger.WarnLine ("[WARN]: error during getting field value unifications: " + ex.Message)

+                                                 acc

+                                         | _ -> acc

+                                      ) unifs

+

   (* --- function body starts here --- *)

   let unifs = GetArgValueUnifications (GetMethodInArgs m)

-  let fldNames = if IsConstructor m then [] else GetConcreteFields comp |> List.map (function Var(name,_) -> name)

-  let unifs2 = GetFldValueUnifications fldNames unifs

-  GetUnifications indent (comp,m) heapInst unifs2 (GetMethodPrePost m |> fun x -> BinaryAnd (fst x) (snd x))

+  let unifs = 

+    //TODO: it should really read the "modifies" clause and figure out modifiable fields from there

+    if not (IsConstructor m) then 

+      GetFldValueUnifications unifs

+    else

+      unifs

+  GetUnifications prog indent (comp,m) heapInst unifs (GetMethodPrePost m |> fun x -> BinaryAnd (fst x) (snd x))

 

 //  =======================================================

 /// Applies given unifications onto the given heap/env/ctx

@@ -308,7 +321,7 @@ let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative =
       let heapInst = ApplyUnifications indent prog comp mthd rest heapInst conservative

       let newHeap = heapInst.assignments|> List.fold (fun acc asgn ->

                                                         match asgn with

-                                                        | FieldAssignment((o,f),value) ->

+                                                        | FieldAssignment((o,f),value) when heapInst.modifiableObjs |> Set.contains o ->

                                                             let e2 = __Apply (o,f) c e value

                                                             acc @ [FieldAssignment((o,f),e2)] 

                                                         | _ -> acc @ [asgn]

@@ -341,25 +354,57 @@ let rec DiscoverAliasing exprList heapInst =
       BinaryAnd eqExpr (DiscoverAliasing rest heapInst)

   | [] -> TrueLiteral

 

-// use the orginal method, not the one with an extra precondition

-let FixSolution origComp origMeth sol =

-  sol |> Map.fold (fun acc (cc,mm) v -> 

-                      if CheckSameMethods (cc,mm) (origComp,origMeth) then

-                        acc |> Map.add (origComp,origMeth) v

-                      else 

-                        acc |> Map.add (cc,mm) v) Map.empty

-

 //

 let DontResolveUnmodifiableStuff prog comp meth expr =

   let methodArgs = GetMethodInArgs meth

   let __IsMethodArg argName = methodArgs |> List.exists (fun (Var(vname,_)) -> vname = argName)

-  let isConstr = match meth with Method(_,_,_,_,b) -> b | _ -> false

+  let isConstr = IsConstructor meth

   match expr with

   | VarLiteral(id) when __IsMethodArg id -> false 

-  | IdLiteral(id) when not (id = "this" || id = "null") -> isConstr

-  | Dot(lhs, fldName) -> isConstr

+  | IdLiteral(id) when id = "this" || id = "null" -> true

+  | IdLiteral(id) | Dot(_, id) -> 

+      // this must be a field, so resolve it only if constructor

+      isConstr

   | _ -> true

 

+/// Descends down a given expression and returns all sub-expressions that evaluate to TrueLiteral

+let FindTrueClauses prog comp m heapInst expr = 

+  let MyFun expr acc =

+    try 

+      let exprEval = Eval heapInst (DontResolveUnmodifiableStuff prog comp m) expr

+      if exprEval = TrueLiteral then

+        acc

+      else

+        let exprAllResolved = Eval heapInst (fun _ -> true) expr

+        match exprAllResolved with

+        | BoolLiteral(true) -> acc @ [exprEval]

+        | _ -> acc

+    with

+    | _ -> acc

+  (* --- function body starts here --- *)

+  DescendExpr2 MyFun expr []

+

+/// Returns a list of boolean expressions obtained by combining (in some way) 

+/// the two given list of conditions conditions

+let GetAllPossibleConditions specConds argConds aliasingConds = 

+  let __Conjoin lst = lst |> List.fold (fun acc e -> BinaryAnd acc e) TrueLiteral

+  let __Preproc lst = lst |> List.map SplitIntoConjunts |> List.concat |> Utils.ListDeduplicate

+

+  // 0. aliasing conditions

+  // 1. conjunction of spec conditions

+  // 2. individual arg conditions

+  // 3. conjunction of arg conditions

+  // 4. individual spec conditions

+  let aliasing = aliasingConds |> __Preproc

+  let specIndi = specConds |> __Preproc

+  let specConj = [__Conjoin specIndi]

+  let argsIndi = argConds |> __Preproc

+  let argsConj = [__Conjoin argsIndi]

+  

+  let allConds = aliasing @ specConj @ argsIndi @ specIndi @ argsConj

+  allConds |> List.filter (fun e -> not (e = TrueLiteral)) 

+           |> Utils.ListDeduplicate

+

 //  ============================================================================

 /// Attempts to synthesize the initialization code for the given constructor "m"

 ///

@@ -392,7 +437,7 @@ let rec AnalyzeConstructor indent prog comp m callGraph =
         let model = models.[0]

         let hModel = ReadFieldValuesFromModel model prog comp m

         let heapInst = ResolveModel hModel m

-        let unifs = GetUnificationsForMethod indent comp m heapInst |> Map.toList

+        let unifs = GetUnificationsForMethod indent prog comp m heapInst |> Map.toList

         let heapInst = ApplyUnifications indent prog comp m unifs heapInst true

         

         // split into method calls

@@ -413,81 +458,137 @@ let rec AnalyzeConstructor indent prog comp m callGraph =
             else

               sol      

         else

-          sol

+          sol             

 and TryInferConditionals indent prog comp m unifs heapInst callGraph = 

+  let rec __TryOutConditions candidateConditions =

+    let idt = Indent indent

+    match candidateConditions with 

+    | [] ->

+        Logger.InfoLine (sprintf "%s    - no more interesting pre-conditions" idt)

+        None

+    | candCond :: rest ->

+        Logger.InfoLine (sprintf "%s    ________________________" idt)

+        Logger.InfoLine (sprintf "%s    candidate pre-condition: %s" idt (PrintExpr 0 candCond))

+        Logger.InfoLine (sprintf "%s    ------------------------" idt)

+        let idt = idt + "  "

+        let _,_,m2 = AddPrecondition prog comp m candCond

+        let sol = MakeModular (indent+2) prog comp m2 candCond heapInst callGraph

+        Logger.Info (idt + "    - verifying partial solution ... ")

+        let verified = 

+          if Options.CONFIG.verifyPartialSolutions then

+            VerifySolution prog sol Options.CONFIG.genRepr

+          else 

+            true

+        if verified then

+          if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED"

+          Some(candCond,m2,sol)

+        else 

+          Logger.InfoLine "NOT VERIFIED"

+          __TryOutConditions rest

+

+  (* --- function body starts here --- *) 

   let idt = Indent indent

   let wrongSol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst]

   let heapInst2 = ApplyUnifications indent prog comp m unifs heapInst false

   let methodArgs = GetMethodInArgs m

+  

+  // find candidate conditions

   let expr = GetHeapExpr prog m heapInst2

-  // now evaluate and see what's left

-  // printf "%s" (expr |> SplitIntoConjunts |> PrintSep newline (fun e -> PrintExpr 0 e))

-  let newCond = Eval heapInst2 (DontResolveUnmodifiableStuff prog comp m) expr

-  if newCond = TrueLiteral then

-    Logger.InfoLine (sprintf "%s    - no more interesting pre-conditions" idt)

-    wrongSol

+  let specConds = expr |> FindTrueClauses prog comp m heapInst2

+  let specConds = specConds 

+                       |> List.filter (IsUnmodConcrOnly prog (comp,m))

+

+  let aliasingCond = lazy(DiscoverAliasing (methodArgs |> List.map (function Var(name,_) -> VarLiteral(name))) heapInst2) 

+  let argConds = heapInst2.methodArgs |> Map.fold (fun acc name value -> acc @ [BinaryEq (VarLiteral(name)) (Const2Expr value)]) []

+  let allConds = GetAllPossibleConditions specConds argConds [aliasingCond.Force()]

+    

+  // --- trace

+  let loggerFunc = fun e -> Logger.TraceLine (sprintf "%s    --> %s" idt (PrintExpr 0 e))

+  allConds |> List.iter loggerFunc

+  // ---

+                      

+  if IsSolution1stLevelOnly heapInst2 then

+    // try to find a non-recursive solution

+    match __TryOutConditions allConds with

+    | Some(candCond,m2,sol) ->

+        let solThis = match TryFindExistingAndConvertToSolution indent comp m2 candCond callGraph with

+                      | Some(sol2) -> sol2

+                      | None -> sol   

+        let _,_,m3 = AddPrecondition prog comp m (UnaryNot(candCond))

+        let solRest = AnalyzeConstructor (indent + 2) prog comp m3 callGraph

+        MergeSolutions solThis solRest |> FixSolution comp m

+    | None -> 

+        Logger.InfoLine (idt + "!!! Giving up !!!")

+        wrongSol

+

+    // let newCond = Eval heapInst2 (DontResolveUnmodifiableStuff prog comp m) expr

+//    match newConds with 

+//    | [] ->

+//        Logger.InfoLine (sprintf "%s    - no more interesting pre-conditions" idt)

+//        wrongSol

+//    | _ ->

+//        //if not (rest = []) then Logger.WarnLine ("[WARN] NOT IMPLEMENTED YET: more than candidate condition ") //TODO

+//        let candCond = newConds |> List.fold BinaryAnd TrueLiteral    //TODO: do some search or something

+//        Logger.InfoLine (sprintf "%s    - candidate pre-condition: %s" idt (PrintExpr 0 candCond))

+//        let _,_,m2 = AddPrecondition prog comp m candCond

+//        let sol = MakeModular indent prog comp m2 candCond heapInst2 callGraph

+//        Logger.Info (idt + "    - verifying partial solution ... ")

+//        let verified = 

+//          if Options.CONFIG.verifyPartialSolutions then

+//            VerifySolution prog sol Options.CONFIG.genRepr

+//          else 

+//            true

+//        if verified then

+//          if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED"

+//          let solThis = match TryFindExistingAndConvertToSolution indent comp m2 candCond callGraph with

+//                        | Some(sol2) -> sol2

+//                        | None -> sol   

+//          let _,_,m3 = AddPrecondition prog comp m (UnaryNot(candCond))

+//          let solRest = AnalyzeConstructor (indent + 2) prog comp m3 callGraph

+//          MergeSolutions solThis solRest |> FixSolution comp m

+//        else 

+//          Logger.InfoLine "NOT VERIFIED"

+//          wrongSol  

   else

-    let candCond = 

-      if newCond = FalseLiteral then

-        // it must be because there is some aliasing going on between method arguments, 

-        // so we should try that as a candidate pre-condition

-        let tmp = DiscoverAliasing (methodArgs |> List.map (function Var(name,_) -> VarLiteral(name))) heapInst2

-        if tmp = TrueLiteral then failwith ("post-condition evaluated to false and no aliasing was discovered")

-        tmp

-      else 

-        newCond

-    Logger.InfoLine (sprintf "%s    - candidate pre-condition: %s" idt (PrintExpr 0 candCond))

-    let _,_,m2 = AddPrecondition prog comp m candCond

-    let sol = MakeModular indent prog comp m2 candCond heapInst2 callGraph

-    Logger.Info (idt + "    - verifying partial solution ... ")

-    let verified = 

-      if Options.CONFIG.verifyPartialSolutions then

-        VerifySolution prog sol Options.CONFIG.genRepr

-      else 

-        true

-    if verified then

-      if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED"

-      let solThis = match TryFindExistingAndConvertToSolution indent comp m2 candCond callGraph with

-                    | Some(sol2) -> sol2

-                    | None -> sol   

-      let _,_,m3 = AddPrecondition prog comp m (UnaryNot(candCond))

-      let solRest = AnalyzeConstructor (indent + 2) prog comp m3 callGraph

-      MergeSolutions solThis solRest |> FixSolution comp m

-    else 

-      Logger.InfoLine "NOT VERIFIED"

-      wrongSol  

-      

+    // the solution is not immediate, so try to delegate to a method call, possibly to a recursive one

+    //TODO

+    Logger.InfoLine "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%"

+    wrongSol    

+

 let GetMethodsToAnalyze prog =

-  let mOpt = Options.CONFIG.methodToSynth;

-  if mOpt = "*" then

-    (* all *)

-    FilterMembers prog FilterMethodMembers // FilterConstructorMembers

-  elif mOpt = "paramsOnly" then

-    (* only with parameters *)

-    FilterMembers prog FilterConstructorMembersWithParams 

-  else

-    let allMethods,neg = 

-      if mOpt.StartsWith("~") then

-        mOpt.Substring(1), true

-      else

-        mOpt, false

-    (* exact list *)

-    let methods = allMethods.Split([|','|])

-    let lst = methods |> Array.fold (fun acc m -> 

-                                       let idx = m.LastIndexOf(".")

-                                       if idx = -1 || idx = m.Length - 1 then

-                                         raise (InvalidCmdLineArg("Invalid method full name: " + m))

-                                       let compName = m.Substring(0, idx)

-                                       let methName = m.Substring(idx + 1)

-                                       let c = FindComponent prog compName |> Utils.ExtractOptionMsg ("Cannot find component " + compName)

-                                       let mthd = FindMethod c methName |> Utils.ExtractOptionMsg ("Cannot find method " + methName + " in component " + compName)

-                                       (c,mthd) :: acc

-                                    ) []

-    if neg then

-      FilterMembers prog FilterConstructorMembers |> List.filter (fun e -> not (Utils.ListContains e lst))

+  let __ReadMethodsParam = 

+    let mOpt = Options.CONFIG.methodToSynth;

+    if mOpt = "*" then

+      (* all *)

+      FilterMembers prog FilterMethodMembers

     else

-      lst

-  

+      let allMethods,neg = 

+        if mOpt.StartsWith("~") then

+          mOpt.Substring(1), true

+        else

+          mOpt, false

+      (* exact list *)

+      let methods = allMethods.Split([|','|])

+      let lst = methods |> Array.fold (fun acc m -> 

+                                         let idx = m.LastIndexOf(".")

+                                         if idx = -1 || idx = m.Length - 1 then

+                                           raise (InvalidCmdLineArg("Invalid method full name: " + m))

+                                         let compName = m.Substring(0, idx)

+                                         let methName = m.Substring(idx + 1)

+                                         let c = FindComponent prog compName |> Utils.ExtractOptionMsg ("Cannot find component " + compName)

+                                         let mthd = FindMethod c methName |> Utils.ExtractOptionMsg ("Cannot find method " + methName + " in component " + compName)

+                                         (c,mthd) :: acc

+                                      ) []

+      if neg then

+        FilterMembers prog FilterMethodMembers |> List.filter (fun e -> not (Utils.ListContains e lst))

+      else

+        lst

+  (* --- function body starts here --- *)

+  let meths = __ReadMethodsParam

+  if Options.CONFIG.constructorsOnly then

+    meths |> List.filter (fun (c,m) -> IsConstructor m)

+  else 

+    meths

 

 // ============================================================================

 /// Goes through a given list of methods of the given program and attempts to 

diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index a866ad08..b4ed22e6 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -147,8 +147,11 @@ let rec DescendExpr2 visitorFunc expr acc =
   | SequenceExpr(exs)                

   | SetExpr(exs)                     -> __Pipe exs

 

-let PrintGenSym name =

-  sprintf "gensym%s" name

+let PrintGenSym (name: string) =

+  if name.StartsWith("gensym") then

+    name

+  else

+    sprintf "gensym%s" name

 

 //  =====================

 /// Returns TRUE literal

@@ -168,6 +171,7 @@ let UnaryNeg sub =
 let UnaryNot sub =

   match sub with

   | UnaryExpr("!", s) -> s

+  | BoolLiteral(b) -> BoolLiteral(not b)

   | _ -> UnaryExpr("!", sub)

 

 //  =======================================================================

@@ -203,7 +207,7 @@ let BinaryOr (lhs: Expr) (rhs: Expr) =
 //  ===================================================================================

 let BinaryImplies lhs rhs = 

   match lhs, rhs with

-  | BoolLiteral(false), _ -> FalseLiteral

+  | BoolLiteral(false), _ -> TrueLiteral

   | BoolLiteral(true), _  -> rhs

   | _, BoolLiteral(true)  -> lhs

   | _, BoolLiteral(false) -> UnaryNot(lhs)

@@ -266,9 +270,10 @@ let rec Expr2Const e =
   match e with

   | IntLiteral(n) -> IntConst(n)

   | BoolLiteral(b) -> BoolConst(b)

+  | BoxLiteral(id) -> BoxConst(id)

   | ObjLiteral("this") -> ThisConst("this",None)

   | ObjLiteral("null") -> NullConst

-  | ObjLiteral(name) -> Unresolved(name)

+  | ObjLiteral(name) -> NewObj(name, None)

   | IdLiteral(id) -> Unresolved(id)

   | VarLiteral(id) -> VarConst(id)

   | SequenceExpr(elist) -> SeqConst(elist |> List.map Expr2Const)

@@ -358,6 +363,9 @@ let rec GroupFieldsByType fields =
       let fldSet = Map.tryFind ty map |> Utils.ExtractOptionOr Set.empty

       map |> Map.add ty (fldSet |> Set.add (Var(name, ty)))

   | [] -> Map.empty

+ 

+let IsConcreteField comp fldName = GetConcreteFields comp |> List.exists (function Var(name,_) -> name = fldName)

+let IsAbstractField comp fldName = GetAbstractFields comp |> List.exists (function Var(name,_) -> name = fldName)

                     

 //  =================================

 /// Returns class name of a component

@@ -475,6 +483,9 @@ let FindComponent (prog: Program) clsName =
   | Program(comps) -> comps |> List.filter (function Component(Class(name,_,_),_,_) when name = clsName -> true | _ -> false)

                             |> Utils.ListToOption

 

+let FindComponentForType prog ty = 

+  FindComponent prog (GetTypeShortName ty)

+

 //  ===================================================

 /// Finds a method of a component that has a given name

 //  ===================================================

@@ -580,245 +591,243 @@ let __CheckEqual e1 e2 =
   | _ when e1 = e2 -> Some(true)

   | _ -> None

 

-let rec __EvalSym resolverFunc ctx expr = 

-  match expr with

-  | IntLiteral(_)  -> expr

-  | BoolLiteral(_) -> expr

-  | BoxLiteral(_)  -> expr

-  | ObjLiteral(_)  -> expr

-  | Star           -> expr //TODO: can we do better?

-  | VarDeclExpr(_) -> expr

-  | AssertExpr(e)  -> AssertExpr(__EvalSym resolverFunc ctx e)

-  | AssumeExpr(e)  -> AssumeExpr(__EvalSym resolverFunc ctx e)

-  | VarLiteral(id) -> 

-      try 

-        let _,e = ctx |> List.find (fun (v,e) -> GetVarName v = id)

-        e

-      with 

-      | ex -> resolverFunc expr None

-  | IdLiteral(_)   -> resolverFunc expr None

-  | Dot(e, str)    -> 

-      let discr = __EvalSym resolverFunc ctx e

-      resolverFunc discr (Some(str))

-  | SeqLength(e)   -> 

-      let e' = __EvalSym resolverFunc ctx e

-      match e' with

-      | SequenceExpr(elist) -> IntLiteral(List.length elist)

-      | _ -> SeqLength(e')

-  | SequenceExpr(elist) -> 

-      let elist' = elist |> List.fold (fun acc e -> __EvalSym resolverFunc ctx e :: acc) [] |> List.rev

-      SequenceExpr(elist')

-  | SetExpr(elist) -> 

-      let eset' = elist |> List.fold (fun acc e -> Set.add (__EvalSym resolverFunc ctx e) acc) Set.empty

-      SetExpr(Set.toList eset')

-  | MethodCall(rcv,cname, mname,aparams) ->

-      let rcv' = __EvalSym resolverFunc ctx rcv

-      let aparams' = aparams |> List.fold (fun acc e -> __EvalSym resolverFunc ctx e :: acc) [] |> List.rev

-      MethodCall(rcv', cname, mname, aparams')

-  | LCIntervalExpr(_) -> expr

-  | SelectExpr(lst, idx) ->

-      let lst' = __EvalSym resolverFunc ctx lst

-      let idx' = __EvalSym resolverFunc ctx idx 

-      match lst', idx' with

-      | SequenceExpr(elist), IntLiteral(n) -> elist.[n] 

-      | SequenceExpr(elist), LCIntervalExpr(startIdx) ->

-          let startIdx' = __EvalSym resolverFunc ctx startIdx

-          match startIdx' with

-          | IntLiteral(startIdxInt) -> 

-              let rec __Skip n l = if n = 0 then l else __Skip (n-1) (List.tail l)

-              SequenceExpr(__Skip startIdxInt elist)

-          | _ -> SelectExpr(lst', idx')

-      | _ -> SelectExpr(lst', idx')

-  | UpdateExpr(lst,idx,v) ->

-      let lst', idx', v' = __EvalSym resolverFunc ctx lst, __EvalSym resolverFunc ctx idx, __EvalSym resolverFunc ctx v

-      match lst', idx', v' with

-      | SequenceExpr(elist), IntLiteral(n), _ -> SequenceExpr(Utils.ListSet n v' elist)

-      | _ -> UpdateExpr(lst', idx', v')

-  | IteExpr(c, e1, e2) ->

-      let c' = __EvalSym resolverFunc ctx c

-      match c' with

-      | BoolLiteral(b) -> if b then __EvalSym resolverFunc ctx e1 else __EvalSym resolverFunc ctx e2

-      | _ -> IteExpr(c', __EvalSym resolverFunc ctx e1, __EvalSym resolverFunc ctx e2)

-  | BinaryExpr(p,op,e1,e2) ->

-      let e1' = lazy (__EvalSym resolverFunc ctx e1)

-      let e2' = lazy (__EvalSym resolverFunc ctx e2)

-      let recomposed = lazy (BinaryExpr(p, op, e1'.Force(), e2'.Force()))

-      match op with

-      | "=" ->

-          let e1'' = e1'.Force()

-          let e2'' = e2'.Force()

-          let eq = __CheckEqual e1'' e2''

-          match eq with

-          | Some(b) -> BoolLiteral(b)

-          | None -> recomposed.Force()

-      | "!=" -> 

-          let e1'' = e1'.Force()

-          let e2'' = e2'.Force()

-          let eq = __CheckEqual e1'' e2''

-          match eq with

-          | Some(b) -> BoolLiteral(not b)

-          | None -> recomposed.Force()

-      | "<" -> 

-          match e1'.Force(), e2'.Force() with

-          | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 < n2)

-          | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) < (List.length s2))

-          | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) < (List.length s2))

-          | _ -> recomposed.Force()

-      | "<=" -> 

-          let e1'' = e1'.Force()

-          let e2'' = e2'.Force()

-          let eq = __CheckEqual e1'' e2''

-          match eq with

-          | Some(true) -> TrueLiteral

-          | _ -> match e1'', e2'' with

-                 | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 <= n2)

-                 | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) <= (List.length s2))

-                 | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2))

-                 | _ -> recomposed.Force()

-      | ">" -> 

-          match e1'.Force(), e2'.Force() with

-          | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 > n2)

-          | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) > (List.length s2))

-          | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) > (List.length s2))

-          | _ -> recomposed.Force()

-      | ">=" -> 

-          let e1'' = e1'.Force()

-          let e2'' = e2'.Force()

-          let eq = __CheckEqual e1'' e2''

-          match eq with

-          | Some(true) -> TrueLiteral

-          | _ -> match e1'', e2'' with

-                 | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 >= n2)

-                 | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) >= (List.length s2))

-                 | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2))

-                 | _ -> recomposed.Force()

-      | ".." ->

-          let e1'' = e1'.Force()

-          let e2'' = e2'.Force()

-          match e1'', e2'' with

-          | IntLiteral(lo), IntLiteral(hi)    -> SequenceExpr([lo .. hi] |> List.map (fun n -> IntLiteral(n)))

-          | _ -> recomposed.Force();

-      | "in" -> 

-          match e1'.Force(), e2'.Force() with

-          | _, SetExpr(s)       

-          | _, SequenceExpr(s)  -> BoolLiteral(Utils.ListContains (e1'.Force()) s)

-          | _ -> recomposed.Force()

-      | "!in" -> 

-          match e1'.Force(), e2'.Force() with

-          | _, SetExpr(s)       

-          | _, SequenceExpr(s)  -> BoolLiteral(not (Utils.ListContains (e1'.Force()) s))

-          | _ -> recomposed.Force()

-      | "+" -> 

-          let e1'' = e1'.Force();

-          let e2'' = e2'.Force();

-          match e1'', e2'' with

-          | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 + n2)

-          | SequenceExpr(l1), SequenceExpr(l2) -> SequenceExpr(List.append l1 l2)

-          | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.union (Set.ofList s1) (Set.ofList s2) |> Set.toList)

-          | SetExpr(s), _ -> SetExpr(Set.add e2'' (Set.ofList s) |> Set.toList)

-          | _, SetExpr(s) -> SetExpr(Set.add e1'' (Set.ofList s) |> Set.toList)

-          | _ -> recomposed.Force()

-      | "-" -> 

-          match e1'.Force(), e2'.Force() with

-          | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 - n2)

-          | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.difference (Set.ofList s1) (Set.ofList s2) |> Set.toList)

-          | _ -> recomposed.Force()

-      | "*" -> 

-          match e1'.Force(), e2'.Force() with

-          | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 * n2)

-          | _ -> recomposed.Force()

-      | "div" -> 

-          match e1'.Force(), e2'.Force() with

-          | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 / n2)

-          | _ -> recomposed.Force()

-      | "mod" -> 

-          match e1'.Force(), e2'.Force() with

-          | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 % n2)

-          | _ -> recomposed.Force()

-      | "&&" -> 

-          // shortcircuit

-          match e1'.Force() with

-          | BoolLiteral(false) -> BoolLiteral(false)

-          | _ ->

-              match e1'.Force(), e2'.Force() with

-              | BoolLiteral(false), _            -> BoolLiteral(false)

-              | _, BoolLiteral(false)            -> BoolLiteral(false)

-              | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 && b2)

-              | _ -> BinaryAnd (e1'.Force()) (e2'.Force())

-      | "||" -> 

-          // shortcircuit

-          match e1'.Force() with

-          | BoolLiteral(true) -> BoolLiteral(true)

-          | _ ->

-              match e1'.Force(), e2'.Force() with

-              | BoolLiteral(true), _             -> BoolLiteral(true)

-              | _, BoolLiteral(true)             -> BoolLiteral(true)

-              | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 || b2)

-              | _ -> BinaryOr (e1'.Force()) (e2'.Force())

-      | "==>" -> 

-          // shortcircuit

-          match e1'.Force() with

-          | BoolLiteral(false) -> BoolLiteral(true)

-          | _ ->

-              let e1'' = e1'.Force()

-              let e2'' = e2'.Force()

-              match e1'', e2'' with

-              | BoolLiteral(false), _            -> BoolLiteral(true)

-              | _, BoolLiteral(true)             -> BoolLiteral(true)

-              | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral((not b1) || b2)

-              | _ -> BinaryImplies (e1'.Force()) (e2'.Force())

-      | "<==>" -> 

-          match e1'.Force(), e2'.Force() with

-          | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 = b2)

-          | x, BoolLiteral(b)

-          | BoolLiteral(b), x -> if b then x else UnaryNot(x)

-          | _ -> recomposed.Force()

-      | _ -> recomposed.Force()

-  | UnaryExpr(op, e) ->

-      let e' = __EvalSym resolverFunc ctx e

-      let recomposed = UnaryExpr(op, e')

-      match op with

-      | "!" -> 

-          match e' with

-          | BoolLiteral(b) -> BoolLiteral(not b)

-          | _ -> recomposed

-      | "-" -> 

-          match e' with

-          | IntLiteral(n) -> IntLiteral(-n)

-          | _ -> recomposed

-      | _ -> recomposed

-  | ForallExpr(vars, e) -> 

-      let rec __ExhaustVar v restV vDomain = 

-        match vDomain with

-        | vv :: restD -> 

-            let ctx' = (v,vv) :: ctx

-            let e' = __EvalSym resolverFunc ctx' (ForallExpr(restV, e))

-            let erest = __ExhaustVar v restV restD

-            (* __EvalSym resolverFunc ctx' *) 

-            BinaryAnd e' erest

-        | [] -> BoolLiteral(true)

-      let rec __TraverseVars vars =

-        match vars with

-        | v :: restV -> 

-            try 

-              let vDom = GetVarDomain resolverFunc ctx v e

-              __ExhaustVar v restV vDom

-            with

-              | ex -> ForallExpr([v], __TraverseVars restV) 

-        | [] -> __EvalSym resolverFunc ctx e

-      (* --- function body starts here --- *)

-      __TraverseVars vars

-and GetVarDomain resolverFunc ctx var expr = 

+let rec __EvalSym resolverFunc returnFunc ctx expr =

+  let expr' = 

+    match expr with

+    | IntLiteral(_)  -> expr 

+    | BoolLiteral(_) -> expr 

+    | BoxLiteral(_)  -> expr 

+    | ObjLiteral(_)  -> expr 

+    | Star           -> expr  //TODO: can we do better?

+    | VarDeclExpr(_) -> expr 

+    | AssertExpr(e)  -> AssertExpr(__EvalSym resolverFunc returnFunc ctx e) 

+    | AssumeExpr(e)  -> AssumeExpr(__EvalSym resolverFunc returnFunc ctx e) 

+    | VarLiteral(id) -> 

+        try 

+          let _,e = ctx |> List.find (fun (v,e) -> GetVarName v = id)

+          e 

+        with 

+        | ex -> resolverFunc expr None 

+    | IdLiteral(_)   -> resolverFunc expr None 

+    | Dot(e, str)    -> 

+        let discr = __EvalSym resolverFunc returnFunc ctx e

+        resolverFunc discr (Some(str)) 

+    | SeqLength(e)   -> 

+        let e' = __EvalSym resolverFunc returnFunc ctx e

+        match e' with

+        | SequenceExpr(elist) -> IntLiteral(List.length elist) 

+        | _ -> SeqLength(e') 

+    | SequenceExpr(elist) -> 

+        let elist' = elist |> List.fold (fun acc e -> (__EvalSym resolverFunc returnFunc ctx e) :: acc) [] |> List.rev

+        SequenceExpr(elist') 

+    | SetExpr(elist) -> 

+        let eset' = elist |> List.fold (fun acc e -> Set.add (__EvalSym resolverFunc returnFunc ctx e) acc) Set.empty

+        SetExpr(Set.toList eset') 

+    | MethodCall(rcv,cname, mname,aparams) ->

+        let rcv' = __EvalSym resolverFunc returnFunc ctx rcv

+        let aparams' = aparams |> List.fold (fun acc e -> __EvalSym resolverFunc returnFunc ctx e :: acc) [] |> List.rev

+        MethodCall(rcv', cname, mname, aparams') 

+    | LCIntervalExpr(_) -> expr 

+    | SelectExpr(lst, idx) ->

+        let lst' = __EvalSym resolverFunc returnFunc ctx lst

+        let idx' = __EvalSym resolverFunc returnFunc ctx idx 

+        match lst', idx' with

+        | SequenceExpr(elist), IntLiteral(n) -> elist.[n] 

+        | SequenceExpr(elist), LCIntervalExpr(startIdx) ->

+            let startIdx' = __EvalSym resolverFunc returnFunc ctx startIdx

+            match startIdx' with

+            | IntLiteral(startIdxInt) -> 

+                let rec __Skip n l = if n = 0 then l else __Skip (n-1) (List.tail l)

+                SequenceExpr(__Skip startIdxInt elist)

+            | _ -> SelectExpr(lst', idx')

+        | _ -> SelectExpr(lst', idx')

+    | UpdateExpr(lst,idx,v) ->

+        let lst', idx', v' = __EvalSym resolverFunc returnFunc ctx lst, __EvalSym resolverFunc returnFunc ctx idx, __EvalSym resolverFunc returnFunc ctx v

+        match lst', idx', v' with

+        | SequenceExpr(elist), IntLiteral(n), _ -> SequenceExpr(Utils.ListSet n v' elist)

+        | _ -> UpdateExpr(lst', idx', v')

+    | IteExpr(c, e1, e2) ->

+        let c' = __EvalSym resolverFunc returnFunc ctx c

+        match c' with

+        | BoolLiteral(b) -> if b then __EvalSym resolverFunc returnFunc ctx e1 else __EvalSym resolverFunc returnFunc ctx e2

+        | _ -> IteExpr(c', __EvalSym resolverFunc returnFunc ctx e1, __EvalSym resolverFunc returnFunc ctx e2)

+    | BinaryExpr(p,op,e1,e2) ->

+        let e1' = lazy (__EvalSym resolverFunc returnFunc ctx e1)

+        let e2' = lazy (__EvalSym resolverFunc returnFunc ctx e2)

+        let recomposed = lazy (BinaryExpr(p, op, e1'.Force(), e2'.Force()))

+        match op with

+        | "=" ->

+            let e1'' = e1'.Force()

+            let e2'' = e2'.Force()

+            let eq = __CheckEqual e1'' e2''

+            match eq with

+            | Some(b) -> BoolLiteral(b)

+            | None -> recomposed.Force()

+        | "!=" -> 

+            let e1'' = e1'.Force()

+            let e2'' = e2'.Force()

+            let eq = __CheckEqual e1'' e2''

+            match eq with

+            | Some(b) -> BoolLiteral(not b)

+            | None -> recomposed.Force()

+        | "<" -> 

+            match e1'.Force(), e2'.Force() with

+            | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 < n2)

+            | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) < (List.length s2))

+            | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) < (List.length s2))

+            | _ -> recomposed.Force()

+        | "<=" -> 

+            let e1'' = e1'.Force()

+            let e2'' = e2'.Force()

+            let eq = __CheckEqual e1'' e2''

+            match eq with

+            | Some(true) -> TrueLiteral

+            | _ -> match e1'', e2'' with

+                   | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 <= n2)

+                   | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) <= (List.length s2))

+                   | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2))

+                   | _ -> recomposed.Force()

+        | ">" -> 

+            match e1'.Force(), e2'.Force() with

+            | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 > n2)

+            | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) > (List.length s2))

+            | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) > (List.length s2))

+            | _ -> recomposed.Force()

+        | ">=" -> 

+            let e1'' = e1'.Force()

+            let e2'' = e2'.Force()

+            let eq = __CheckEqual e1'' e2''

+            match eq with

+            | Some(true) -> TrueLiteral

+            | _ -> match e1'', e2'' with

+                   | IntLiteral(n1), IntLiteral(n2)     -> BoolLiteral(n1 >= n2)

+                   | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) >= (List.length s2))

+                   | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2))

+                   | _ -> recomposed.Force()

+        | ".." ->

+            let e1'' = e1'.Force()

+            let e2'' = e2'.Force()

+            match e1'', e2'' with

+            | IntLiteral(lo), IntLiteral(hi)    -> SequenceExpr([lo .. hi] |> List.map (fun n -> IntLiteral(n)))

+            | _ -> recomposed.Force();

+        | "in" -> 

+            match e1'.Force(), e2'.Force() with

+            | _, SetExpr(s)       

+            | _, SequenceExpr(s)  -> BoolLiteral(Utils.ListContains (e1'.Force()) s)

+            | _ -> recomposed.Force()

+        | "!in" -> 

+            match e1'.Force(), e2'.Force() with

+            | _, SetExpr(s)       

+            | _, SequenceExpr(s)  -> BoolLiteral(not (Utils.ListContains (e1'.Force()) s))

+            | _ -> recomposed.Force()

+        | "+" -> 

+            let e1'' = e1'.Force();

+            let e2'' = e2'.Force();

+            match e1'', e2'' with

+            | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 + n2)

+            | SequenceExpr(l1), SequenceExpr(l2) -> SequenceExpr(List.append l1 l2)

+            | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.union (Set.ofList s1) (Set.ofList s2) |> Set.toList)

+            | SetExpr(s), _ -> SetExpr(Set.add e2'' (Set.ofList s) |> Set.toList)

+            | _, SetExpr(s) -> SetExpr(Set.add e1'' (Set.ofList s) |> Set.toList)

+            | _ -> recomposed.Force()

+        | "-" -> 

+            match e1'.Force(), e2'.Force() with

+            | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 - n2)

+            | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.difference (Set.ofList s1) (Set.ofList s2) |> Set.toList)

+            | _ -> recomposed.Force()

+        | "*" -> 

+            match e1'.Force(), e2'.Force() with

+            | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 * n2)

+            | _ -> recomposed.Force()

+        | "div" -> 

+            match e1'.Force(), e2'.Force() with

+            | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 / n2)

+            | _ -> recomposed.Force()

+        | "mod" -> 

+            match e1'.Force(), e2'.Force() with

+            | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 % n2)

+            | _ -> recomposed.Force()

+        | "&&" -> 

+            // shortcircuit

+            match e1'.Force() with

+            | BoolLiteral(false) -> BoolLiteral(false)

+            | _ ->

+                match e1'.Force(), e2'.Force() with

+                | BoolLiteral(false), _            -> BoolLiteral(false)

+                | _, BoolLiteral(false)            -> BoolLiteral(false)

+                | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 && b2)

+                | _ -> BinaryAnd (e1'.Force()) (e2'.Force())

+        | "||" -> 

+            // shortcircuit

+            match e1'.Force() with

+            | BoolLiteral(true) -> BoolLiteral(true)

+            | _ ->

+                match e1'.Force(), e2'.Force() with

+                | BoolLiteral(true), _             -> BoolLiteral(true)

+                | _, BoolLiteral(true)             -> BoolLiteral(true)

+                | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 || b2)

+                | _ -> BinaryOr (e1'.Force()) (e2'.Force())

+        | "==>" -> 

+            // shortcircuit

+            match e1'.Force() with

+            | BoolLiteral(false) -> BoolLiteral(true)

+            | _ ->

+                let e1'' = e1'.Force()

+                let e2'' = e2'.Force()

+                BinaryImplies e1'' e2''

+        | "<==>" -> 

+            match e1'.Force(), e2'.Force() with

+            | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 = b2)

+            | x, BoolLiteral(b)

+            | BoolLiteral(b), x -> if b then x else UnaryNot(x)

+            | _ -> recomposed.Force()

+        | _ -> recomposed.Force()

+    | UnaryExpr(op, e) ->

+        let e' = __EvalSym resolverFunc returnFunc ctx e

+        let recomposed = UnaryExpr(op, e')

+        match op with

+        | "!" -> 

+            match e' with

+            | BoolLiteral(b) -> BoolLiteral(not b)

+            | _ -> recomposed

+        | "-" -> 

+            match e' with

+            | IntLiteral(n) -> IntLiteral(-n)

+            | _ -> recomposed

+        | _ -> recomposed

+    | ForallExpr(vars, e) -> 

+        let rec __ExhaustVar v restV vDomain = 

+          match vDomain with

+          | vv :: restD -> 

+              let ctx' = (v,vv) :: ctx

+              let e' = __EvalSym resolverFunc returnFunc ctx' (ForallExpr(restV, e))

+              let erest = __ExhaustVar v restV restD

+              (* __EvalSym resolverFunc returnFunc ctx' *) 

+              BinaryAnd e' erest

+          | [] -> BoolLiteral(true)

+        let rec __TraverseVars vars =

+          match vars with

+          | v :: restV -> 

+              try 

+                let vDom = GetVarDomain resolverFunc returnFunc ctx v e

+                __ExhaustVar v restV vDom

+              with

+                | ex -> ForallExpr([v], __TraverseVars restV) 

+          | [] -> __EvalSym resolverFunc returnFunc ctx e

+        (* --- function body starts here --- *)

+        __TraverseVars vars

+  expr' |> returnFunc

+and GetVarDomain resolverFunc returnFunc ctx var expr = 

   match expr with 

   | BinaryExpr(_, "==>", lhs, rhs) -> 

       let conjs = SplitIntoConjunts lhs

       conjs |> List.fold (fun acc e ->

                             match e with

                             | BinaryExpr(_, "in", VarLiteral(vn), rhs) when GetVarName var = vn ->

-                                match __EvalSym resolverFunc ctx rhs with

+                                match __EvalSym resolverFunc returnFunc ctx rhs with

                                 | SetExpr(elist)

                                 | SequenceExpr(elist) -> elist |> List.append acc

-                                | _ -> raise DomainNotInferred

+                                | x -> raise DomainNotInferred

                             | BinaryExpr(_, op, VarLiteral(vn),oth)

                             | BinaryExpr(_, op, oth, VarLiteral(vn)) when GetVarName var = vn && Set.ofList ["<"; "<="; ">"; ">="] |> Set.contains op -> 

                                 failwith "Not implemented yet"

@@ -828,7 +837,10 @@ and GetVarDomain resolverFunc ctx var expr =
       raise DomainNotInferred

 

 let EvalSym resolverFunc expr = 

-  __EvalSym resolverFunc [] expr 

+  __EvalSym resolverFunc (fun e -> e) [] expr 

+

+let EvalSymRet resolverFunc returnFunc expr = 

+  __EvalSym resolverFunc returnFunc [] expr 

   

 //  ==========================================================

 /// Desugars a given expression so that all list constructors 

diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs
index a6caaa6e..10398fa9 100644
--- a/Jennisys/Jennisys/CodeGen.fs
+++ b/Jennisys/Jennisys/CodeGen.fs
@@ -160,24 +160,8 @@ let PrintAllocNewObjects heapInst indent =
 

 let PrintVarAssignments heapInst indent = 

   let idt = Indent indent

-  let fldAssgnsStr = heapInst.assignments |> PrintSep newline (fun asgn ->                                                        

-                                                                 let exprStr = 

-                                                                   match asgn with

-                                                                   | FieldAssignment((o,f),e) ->

-                                                                       let fldName = GetVarName f

-                                                                       if fldName = "" then

-                                                                         PrintStmt (ExprStmt(e)) 0 false

-                                                                       else

-                                                                         PrintStmt (Assign(Dot(ObjLiteral(o.name), fldName), e)) 0 false

-                                                                   | ArbitraryStatement(stmt) ->

-                                                                         PrintStmt stmt 0 false

-                                                                 idt + exprStr)

-  let retValsAssgnsStr = heapInst.methodRetVals |> Map.toList

-                                                |> PrintSep newline (fun (retVarName, retVarVal) ->  

-                                                                       let stmt = Assign(VarLiteral(retVarName), retVarVal)

-                                                                       let assgnStr = PrintStmt stmt 0 false

-                                                                       idt + assgnStr)

-  let str = [fldAssgnsStr; retValsAssgnsStr] |> List.filter (fun s -> not (s = "")) |> PrintSep newline (fun s -> s)

+  let stmts = ConvertToStatements heapInst true

+  let str = stmts |> PrintSep (newline) (fun s -> idt + (PrintStmt s 0 false))

   str + newline

 

 ///

diff --git a/Jennisys/Jennisys/DafnyModelUtils.fs b/Jennisys/Jennisys/DafnyModelUtils.fs
index 65fd97d2..6a8cb727 100644
--- a/Jennisys/Jennisys/DafnyModelUtils.fs
+++ b/Jennisys/Jennisys/DafnyModelUtils.fs
@@ -213,19 +213,16 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
         __ReadSeqIndex model rest (newEnv,newCtx)

     | _ -> (envMap,ctx)

 

-  //TODO: This has become obsolete now, as the Seq#Build function has a different meaning now.

-  //      On the plus site, it might be that it is not necessary to read the model for this function anymore.

   // reads stuff from Seq#Build

   let rec __ReadSeqBuild (model: Microsoft.Boogie.Model) (bld_tuples: Model.FuncTuple list) (envMap,ctx) = 

     match bld_tuples with

     | ft :: rest -> 

         let srcLstLoc = GetLoc ft.Args.[0]

+        let lstElemVal = UnboxIfNeeded model ft.Args.[1]

         let dstLstLoc = GetLoc ft.Result

-        let oldLst = FindSeqInEnv envMap srcLstLoc

-        let idx = GetInt ft.Args.[1]

-        let lstElemVal = UnboxIfNeeded model ft.Args.[2]

+        let oldLst = FindSeqInEnv envMap srcLstLoc        

         let dstLst = FindSeqInEnv envMap dstLstLoc

-        let newLst = Utils.ListBuild oldLst idx lstElemVal dstLst

+        let newLst = oldLst @ [lstElemVal]

         let newCtx = UpdateContext dstLst newLst ctx

         let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst))

         __ReadSeqBuild model rest (newEnv,newCtx)

@@ -241,20 +238,30 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
         let oldLst1 = FindSeqInEnv envMap srcLst1Loc

         let oldLst2 = FindSeqInEnv envMap srcLst2Loc

         let dstLst = FindSeqInEnv envMap dstLstLoc

-        let newLst = List.append oldLst1 oldLst2

+        let newLst = oldLst1 @ oldLst2

         let newCtx = UpdateContext dstLst newLst ctx

         let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst))

         __ReadSeqAppend model rest (newEnv,newCtx)

     | _ -> (envMap,ctx)  

 

+  // keeps reading from Seq#Build and Seq#Append until fixpoint

+  let rec __ReadUntilFixpoint hmodel = 

+    let f_seq_bld = model.MkFunc("Seq#Build", 2)

+    let f_seq_app = model.MkFunc("Seq#Append", 2)

+    let hmodel' = hmodel |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)

+                       |> __ReadSeqAppend model (List.ofSeq f_seq_app.Apps)               

+    if hmodel' = hmodel then

+      hmodel'

+    else

+      __ReadUntilFixpoint hmodel'

+

   let f_seq_len = model.MkFunc("Seq#Length", 1)

   let f_seq_idx = model.MkFunc("Seq#Index", 2)

-  //let f_seq_bld = model.MkFunc("Seq#Build", 4)

-  let f_seq_app = model.MkFunc("Seq#Append", 2)

-  (envMap,ctx) |> __ReadSeqLen model (List.ofSeq f_seq_len.Apps)

-               |> __ReadSeqIndex model (List.ofSeq f_seq_idx.Apps)

-             //  |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)

-               |> __ReadSeqAppend model (List.ofSeq f_seq_app.Apps)

+  let hmodel = (envMap,ctx)

+  let hmodel' = hmodel |> __ReadSeqLen model (List.ofSeq f_seq_len.Apps)

+                       |> __ReadSeqIndex model (List.ofSeq f_seq_idx.Apps)

+  __ReadUntilFixpoint hmodel'  

+  

 

 

 //  =====================================================

diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index a3c92ab7..2613432c 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
     <WarningLevel>3</WarningLevel>

     <PlatformTarget>x86</PlatformTarget>

     <DocumentationFile>bin\Debug\Language.XML</DocumentationFile>

-    <StartArguments>examples/Set.jen /genMod /genRepr /method:Set.Double</StartArguments>

+    <StartArguments>examples/NumberMethods.jen /genMod /genRepr /method:NumberMethods.Min4</StartArguments>

     <StartWorkingDirectory>C:\boogie\Jennisys\Jennisys\</StartWorkingDirectory>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">

diff --git a/Jennisys/Jennisys/Logger.fs b/Jennisys/Jennisys/Logger.fs
index d9df47a7..dbf762cd 100644
--- a/Jennisys/Jennisys/Logger.fs
+++ b/Jennisys/Jennisys/Logger.fs
@@ -16,7 +16,7 @@ let _WARN = 40
 let _ERROR = 20

 let _NONE = 0

 

-let logLevel = _DEBUG

+let logLevel = _ALL

 

 let Log level msg =

   if logLevel >= level then

diff --git a/Jennisys/Jennisys/MethodUnifier.fs b/Jennisys/Jennisys/MethodUnifier.fs
index f12e8dd0..14d4f31f 100644
--- a/Jennisys/Jennisys/MethodUnifier.fs
+++ b/Jennisys/Jennisys/MethodUnifier.fs
@@ -209,6 +209,7 @@ let TryFindExistingAndConvertToSolution indent comp m cond callGraph =
         let hInst = { objs           = Utils.MapSingleton obj.name obj;

                       modifiableObjs = modObjs;

                       assignments    = body; 

+                      concreteValues = body;

                       methodArgs     = Map.empty; 

                       methodRetVals  = Map.empty;

                       globals        = Map.empty }

diff --git a/Jennisys/Jennisys/Modularizer.fs b/Jennisys/Jennisys/Modularizer.fs
index b196d4cb..c6fcaaec 100644
--- a/Jennisys/Jennisys/Modularizer.fs
+++ b/Jennisys/Jennisys/Modularizer.fs
@@ -39,12 +39,12 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
     | SetExpr(elist) -> elist |> List.fold (fun acc2 e2 -> __AddDirectChildren e2 acc2) acc

     | _ -> acc

 

-  let __GetDirectChildren = 

-    let thisRhsExprs = hInst.assignments |> List.choose (function FieldAssignment((obj,_),e) when obj.name = "this" -> Some(e) | _ -> None)

+  let __GetDirectModifiableChildren = 

+    let thisRhsExprs = hInst.assignments |> List.choose (function FieldAssignment((obj,_),e) when obj.name = "this" && Set.contains obj hInst.modifiableObjs  -> Some(e) | _ -> None)

     thisRhsExprs |> List.fold (fun acc e -> __AddDirectChildren e acc) Set.empty 

                  |> Set.toList

 

-  let directChildren = lazy (__GetDirectChildren)

+  let directChildren = lazy (__GetDirectModifiableChildren)

 

   let __IsAbstractField ty var = 

     let builder = CascadingBuilder<_>(false)

@@ -184,7 +184,7 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
                 | Method (mname, msig, mpre, _, isConstr) -> Method(mname, msig, mpre, postSpec, isConstr)

                 | _ -> failwithf "internal error: expected a Method but got %O" meth

     match TryFindExistingAndConvertToSolution indent comp meth' cond callGraph with

-    | Some(sol) -> sol

+    | Some(sol) -> sol |> FixSolution comp meth

     | None -> 

         // if not found, try to split into parts

         let newMthdLst, newHeapInst = __GetModularBranch

diff --git a/Jennisys/Jennisys/Options.fs b/Jennisys/Jennisys/Options.fs
index b61c16da..7aeb131a 100644
--- a/Jennisys/Jennisys/Options.fs
+++ b/Jennisys/Jennisys/Options.fs
@@ -9,18 +9,19 @@ module Options
 open Utils

 

 type Config = {

-   help: bool;

-   inputFilename: string;

-   methodToSynth: string;

-   inferConditionals: bool;

-   verifyPartialSolutions: bool;

-   verifySolutions: bool;

-   checkUnifications: bool;

-   genRepr: bool;

-   genMod: bool;

-   timeout: int;

-   numLoopUnrolls: int;

-   recursiveValid: bool;

+   help                      : bool;

+   inputFilename             : string;

+   methodToSynth             : string;

+   constructorsOnly          : bool;

+   inferConditionals         : bool;

+   verifyPartialSolutions    : bool;

+   verifySolutions           : bool;

+   checkUnifications         : bool;

+   genRepr                   : bool;

+   genMod                    : bool;

+   timeout                   : int;

+   numLoopUnrolls            : int;

+   recursiveValid            : bool;

 }

 

 type CfgOption<'a> = {

@@ -54,6 +55,7 @@ let CheckBool value optName =
 let cfgOptions = [

   { optionName = "help";            optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with help                   =      CheckBool v "help"});           descr = "description not available"; }

   { optionName = "method";          optionType = "string"; optionSetter = (fun v (cfg: Config) -> {cfg with methodToSynth          = CheckNonEmpty v "method"});          descr = "description not available"; }

+  { optionName = "constrOnly";      optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with constructorsOnly       =      CheckBool v "constrOnly"});     descr = "description not available"; }

   { optionName = "inferConds";      optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with inferConditionals      =      CheckBool v "inferConds"});     descr = "description not available"; }

   { optionName = "noInferConds";    optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with inferConditionals      = not (CheckBool v "inferConds")});    descr = "description not available"; }

   { optionName = "verifyParSol";    optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with verifyPartialSolutions =      CheckBool v "verifyParSol"});   descr = "description not available"; }

@@ -98,6 +100,7 @@ let defaultConfig: Config = {
   inputFilename     = "";

   inferConditionals = true;

   methodToSynth     = "*";

+  constructorsOnly  = false;

   verifyPartialSolutions = true;

   verifySolutions   = true;

   checkUnifications = false;

diff --git a/Jennisys/Jennisys/Resolver.fs b/Jennisys/Jennisys/Resolver.fs
index d38fbf7b..711298f9 100644
--- a/Jennisys/Jennisys/Resolver.fs
+++ b/Jennisys/Jennisys/Resolver.fs
@@ -22,7 +22,8 @@ type AssignmentType =
 type HeapInstance = {

    objs: Map<string, Obj>;

    modifiableObjs: Set<Obj>;

-   assignments: AssignmentType list

+   assignments: AssignmentType list;

+   concreteValues: AssignmentType list;

    methodArgs: Map<string, Const>;

    methodRetVals: Map<string, Expr>;

    globals: Map<string, Expr>;

@@ -30,6 +31,29 @@ type HeapInstance = {
 

 let NoObj = { name = ""; objType = NamedType("", []) }

 

+// use the orginal method, not the one with an extra precondition

+let FixSolution origComp origMeth sol =

+  sol |> Map.fold (fun acc (cc,mm) v -> 

+                      if CheckSameMethods (cc,mm) (origComp,origMeth) then

+                        acc |> Map.add (origComp,origMeth) v

+                      else 

+                        acc |> Map.add (cc,mm) v) Map.empty

+

+let ConvertToStatements heapInst onModifiableObjsOnly = 

+  let stmtLst1 = heapInst.assignments |> List.choose (fun asgn ->                                                        

+                                                        match asgn with

+                                                        | FieldAssignment((o,f),e) when (not onModifiableObjsOnly || Set.contains o heapInst.modifiableObjs) ->

+                                                            let fldName = GetVarName f

+                                                            if fldName = "" then

+                                                              Some(ExprStmt(e))

+                                                            else

+                                                              Some(Assign(Dot(ObjLiteral(o.name), fldName), e))

+                                                        | ArbitraryStatement(stmt) -> Some(stmt)

+                                                        | _ -> None)

+  let stmtLst2 = heapInst.methodRetVals |> Map.toList

+                                        |> List.map (fun (retVarName, retVarVal) -> Assign(VarLiteral(retVarName), retVarVal))

+  stmtLst1 @ stmtLst2

+                            

 // resolving values

 exception ConstResolveFailed of string

  

@@ -58,11 +82,12 @@ let rec ResolveCont hModel failResolver cst =
               | Some(c) -> c

               | _ -> failResolver cst hModel

           | None ->

-              // finally, see if it's a method argument

-              let m = hModel.env |> Map.filter (fun k v -> v = u && match k with VarConst(name) -> true | _ -> false) |> Map.toList

-              match m with 

-              | (vc,_) :: [] -> vc

-              | _ -> failResolver cst hModel

+              failResolver cst hModel

+//              // finally, see if it's an *input* (have no way of telling input from output params here) method argument

+//              let m = hModel.env |> Map.filter (fun k v -> v = u && match k with VarConst(name) -> true | _ -> false) |> Map.toList

+//              match m with 

+//              | (vc,_) :: [] -> vc

+//              | _ -> failResolver cst hModel

   | SeqConst(cseq) -> 

       let resolvedLst = cseq |> List.rev |> List.fold (fun acc c -> ResolveCont hModel failResolver c :: acc) []

       SeqConst(resolvedLst)

@@ -95,11 +120,29 @@ let Resolve hModel cst =
 /// Evaluates a given expression with respect to a given heap instance       

 //  ==================================================================

 let Eval heapInst resolveExprFunc expr = 

-  let rec __EvalResolver expr fldNameOpt = 

-    if not (resolveExprFunc expr) then

-      match fldNameOpt with

-      | None -> expr

-      | Some(n) -> Dot(expr, n)

+  let rec __EvalResolver useConcrete resolveExprFunc expr fldNameOpt = 

+    let rec __FurtherResolve expr = 

+      match expr with

+      | SetExpr(elist)      -> SetExpr(elist |> List.map __FurtherResolve)

+      | SequenceExpr(elist) -> SequenceExpr(elist |> List.map __FurtherResolve)

+      | VarLiteral(_) ->

+          try 

+            __EvalResolver useConcrete resolveExprFunc expr None

+          with 

+          | _ -> expr

+      | IdLiteral(id) when not (id = "this" || id = "null") ->

+          try 

+            __EvalResolver useConcrete resolveExprFunc expr None

+          with 

+          | _ -> expr

+      | _ -> expr

+

+    (* --- function body starts here --- *)

+    let ex = match fldNameOpt with

+             | None -> expr

+             | Some(n) -> Dot(expr, n)

+    if not (resolveExprFunc ex) then

+      ex

     else

       match fldNameOpt with

       | None -> 

@@ -111,25 +154,39 @@ let Eval heapInst resolveExprFunc expr =
               | Some(argValue) -> argValue |> Const2Expr

               | None -> 

                   match heapInst.methodRetVals |> Map.tryFind id with

-                  | Some(e) -> e

+                  | Some(e) -> e |> __FurtherResolve

                   | None -> raise (EvalFailed("cannot find value for method parameter " + id))              

           | IdLiteral(id) ->

               let globalVal = heapInst.globals |> Map.tryFind id

               match globalVal with

               | Some(e) -> e

-              | None -> __EvalResolver ThisLiteral (Some(id))      

+              | None -> __EvalResolver useConcrete resolveExprFunc ThisLiteral (Some(id))      

           | _ -> raise (EvalFailed(sprintf "I'm not supposed to resolve %O" expr))

       | Some(fldName) -> 

           match expr with

           | ObjLiteral(objName) -> 

-              let h2 = heapInst.assignments |> List.filter (function FieldAssignment((o, Var(varName,_)), v) -> o.name = objName && varName = fldName | _ -> false)

+              let asgs = if useConcrete then heapInst.concreteValues else heapInst.assignments

+              let h2 = asgs |> List.filter (function FieldAssignment((o, Var(varName,_)), v) -> o.name = objName && varName = fldName | _ -> false)

               match h2 with

-              | FieldAssignment((_,_),x) :: [] -> x

+              | FieldAssignment((_,_),x) :: [] -> __FurtherResolve x

               | _ :: _ -> raise (EvalFailed(sprintf "can't evaluate expression deterministically: %s.%s resolves to multiple locations" objName fldName))

               | [] -> raise (EvalFailed(sprintf "can't find value for %s.%s" objName fldName))  // TODO: what if that value doesn't matter for the solution, and that's why it's not present in the model???

           | _ -> Dot(expr, fldName)

+

   (* --- function body starts here --- *)

-  EvalSym __EvalResolver expr

+  //EvalSym  (__EvalResolver resolveExprFunc) expr

+  EvalSymRet  (__EvalResolver false resolveExprFunc)

+              (fun expr -> 

+                 // TODO: infer type of expr and then re-execute only if its type is Bool

+                 let e1 = EvalSym (__EvalResolver true (fun _ -> true)) expr

+                 match e1 with

+                 | BoolLiteral(b) -> 

+                     if b then

+                       expr

+                     else 

+                       FalseLiteral

+                 | _ -> expr

+              ) expr

 

 //  =====================================================================

 /// Takes an unresolved model of the heap (HeapModel), resolves all 

@@ -165,15 +222,17 @@ let ResolveModel hModel meth =
   let argmap, retvals = hModel.env |> Map.fold (fun (acc1,acc2) k v -> 

                                                   match k with

                                                   | VarConst(name) -> 

+                                                      let resolvedValExpr = Resolve hModel v

                                                       if outArgs |> List.exists (function Var(varName, _) -> varName = name) then

-                                                        acc1, acc2 |> Map.add name (Resolve hModel v |> Const2Expr)

+                                                        acc1, acc2 |> Map.add name (resolvedValExpr |> Const2Expr)

                                                       else

-                                                        acc1 |> Map.add name (Resolve hModel v), acc2

+                                                        acc1 |> Map.add name resolvedValExpr, acc2

                                                   | _ -> acc1, acc2

                                                ) (Map.empty, Map.empty)

   { objs           = objs;

     modifiableObjs = modObjs;

     assignments    = hmap; 

+    concreteValues = hmap;

     methodArgs     = argmap; 

     methodRetVals  = retvals;

     globals        = Map.empty }

@@ -201,4 +260,34 @@ let rec GetCallGraph solutions graph =
                                        ) Set.empty

         let graph' = graph |> Map.add (comp,m) callees

         GetCallGraph rest graph'

-  | [] -> graph
\ No newline at end of file
+  | [] -> graph

+

+//////////////////////////////

+

+let Is1stLevelExpr heapInst expr = 

+  DescendExpr2 (fun expr acc ->

+                  if not acc then

+                    false

+                  else

+                    match expr with

+                    | Dot(discr, fldName) -> 

+                        let obj = Eval heapInst (fun _ -> true) discr

+                        match obj with 

+                        | ObjLiteral(id) -> id = "this"

+                        | _ -> failwithf "Didn't expect the discriminator of a Dot to not be ObjLiteral"

+                    | _ -> true                          

+               ) expr true

+

+let IsSolution1stLevelOnly heapInst = 

+  let rec __IsSol1stLevel stmts = 

+    match stmts with

+    | stmt :: rest -> 

+        match stmt with

+        | Assign(_, e)

+        | ExprStmt(e) -> 

+            let ok = Is1stLevelExpr heapInst e

+            ok && __IsSol1stLevel rest

+        | Block(stmts) -> __IsSol1stLevel (stmts @ rest)

+    | [] -> true

+  (* --- function body starts here --- *)

+  __IsSol1stLevel (ConvertToStatements heapInst true)
\ No newline at end of file
diff --git a/Jennisys/Jennisys/TypeChecker.fs b/Jennisys/Jennisys/TypeChecker.fs
index 8227b693..bc696f43 100644
--- a/Jennisys/Jennisys/TypeChecker.fs
+++ b/Jennisys/Jennisys/TypeChecker.fs
@@ -1,6 +1,7 @@
 module TypeChecker

 

 open Ast

+open AstUtils

 open Printer

 open System.Collections.Generic

 

@@ -39,5 +40,22 @@ let TypeCheck prog =
       Some(Program(clist))

 

 // TODO: implement this

-let InferType prog expr = 

-  NamedType("unknown", [])
\ No newline at end of file
+let rec InferType prog thisComp expr = 

+  let __FindVar comp fldName = 

+    let var = FindVar comp fldName |> Utils.ExtractOption

+    match var with

+    | Var(_, tyOpt) -> 

+        let c = FindComponentForType prog (Utils.ExtractOption tyOpt) |> Utils.ExtractOption

+        Some(c)

+  try 

+    match expr with

+    | ObjLiteral("this") -> Some(thisComp)

+    | ObjLiteral("null") -> None

+    | IdLiteral(id) -> __FindVar thisComp id

+    | Dot(discr, fldName) -> 

+        match InferType prog thisComp discr with

+        | Some(comp) -> __FindVar comp fldName

+        | None -> None

+    | _ -> None

+  with 

+  | ex -> None
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Utils.fs b/Jennisys/Jennisys/Utils.fs
index 156d427c..5cd8af9d 100644
--- a/Jennisys/Jennisys/Utils.fs
+++ b/Jennisys/Jennisys/Utils.fs
@@ -74,6 +74,19 @@ let ListToOptionMsg  lst errMsg =
 

 let ListToOption lst = ListToOptionMsg lst "given list contains more than one element"

 

+let ListDeduplicate lst = 

+  let rec __Dedup lst (visitedSet: System.Collections.Generic.HashSet<_>) acc = 

+    match lst with

+    | fs :: rest ->  

+        let newAcc = 

+          if visitedSet.Add(fs) then

+            acc @ [fs]

+          else

+            acc

+        __Dedup rest visitedSet newAcc

+    | _ -> acc

+  __Dedup lst (new System.Collections.Generic.HashSet<_>()) []

+        

 //  =============================================================

 /// ensures: forall i :: 0 <= i < |lst| ==> ret[i] = Some(lst[i])

 //  =============================================================

diff --git a/Jennisys/Jennisys/examples/List.jen b/Jennisys/Jennisys/examples/List.jen
index bb36c2bb..e056bcfa 100644
--- a/Jennisys/Jennisys/examples/List.jen
+++ b/Jennisys/Jennisys/examples/List.jen
@@ -46,6 +46,10 @@ class Node[T] {
     requires num >= 0
     ensures num >= |list| ==> ret = null
     ensures num < |list| ==> ret != null && ret.list = list[num..]
+
+  method Get(idx: int) returns (ret: T)
+    requires idx >= 0 && idx < |list|
+    ensures ret = list[idx]
 }
 
 model Node[T] {
@@ -56,6 +60,6 @@ model Node[T] {
     next
 
   invariant
-    next = null <==> list = [data]
+    next = null ==> list = [data]
     next != null ==> list = [data] + next.list 
 } 
diff --git a/Jennisys/Jennisys/tmp.out b/Jennisys/Jennisys/tmp.out
deleted file mode 100644
index 9a51a8c8..00000000
--- a/Jennisys/Jennisys/tmp.out
+++ /dev/null
@@ -1,435 +0,0 @@
-// Jennisys, Copyright (c) 2011, Microsoft.

-  [*] Analyzing constructor

-  ------------------------------------------

-      constructor Set.Empty()

-        ensures elems = {};

-  ------------------------------------------

-      - searching for an instance      ... OK 

-      - delegating to method calls     ...

-      - verifying synthesized solution ... 

-      ~~~ VERIFIED ~~~

-

-  [*] Analyzing constructor

-  ------------------------------------------

-      constructor Set.Singleton(t: int)

-        ensures elems = {t};

-  ------------------------------------------

-      - searching for an instance      ... OK 

-      - adding unification t <--> -463

-      - adding unification {t} <--> {-463}

-      - delegating to method calls     ...

-      - verifying synthesized solution ... 

-      ~~~ VERIFIED ~~~

-  [*] Analyzing constructor

-  ------------------------------------------

-      constructor SetNode.Init(x: int)

-        ensures elems = {x};

-  ------------------------------------------

-      - searching for an instance      ... OK 

-      - adding unification x <--> -100

-      - adding unification {x} <--> {-100}

-      - delegating to method calls     ...

-      - verifying synthesized solution ... 

-      ~~~ VERIFIED ~~~

-

-  [*] Analyzing constructor

-  ------------------------------------------

-      constructor Set.Sum(p: int, q: int)

-        ensures elems = {p + q};

-  ------------------------------------------

-      - substitution method found:

-        constructor Set.Singleton(t: int)

-          ensures elems = {t};

-        Unifications: 

-          t -> p + q

-

-  [*] Analyzing constructor

-  ------------------------------------------

-      constructor Set.Double(p: int, q: int)

-        requires p != q;

-        ensures elems = {p q};

-  ------------------------------------------

-      - searching for an instance      ... OK 

-      - adding unification q <--> -760

-      - adding unification p <--> -463

-      - adding unification p != q <--> true

-      - adding unification {p, q} <--> {-760, -463}

-      - delegating to method calls     ...

-      - verifying synthesized solution ... 

-      ~~~ VERIFIED ~~~

-  [*] Analyzing constructor

-  ------------------------------------------

-      constructor SetNode.Double(p: int, q: int)

-        requires p != q;

-        ensures elems = {p q};

-  ------------------------------------------

-      - searching for an instance      ... OK 

-      - adding unification q <--> 215

-      - adding unification p <--> -249

-      - adding unification p != q <--> true

-      - adding unification {p, q} <--> {-249, 215}

-      - delegating to method calls     ...

-      - verifying synthesized solution ... 

-      !!! NOT VERIFIED !!!

-      Strengthening the pre-condition

-          - candidate pre-condition: q > p

-          - delegating to method calls     ...

-          - verifying partial solution ... VERIFIED

-        [*] Analyzing constructor

-        ------------------------------------------

-            constructor SetNode.Double(p: int, q: int)

-              requires p != q;

-              requires !(q > p);

-              ensures elems = {p q};

-        ------------------------------------------

-            - substitution method found:

-              constructor SetNode.DoubleBase(x: int, y: int)

-                requires x > y;

-                ensures elems = {x y};

-              Unifications: 

-                y -> q

-  [*] Analyzing constructor

-  ------------------------------------------

-      constructor SetNode.DoubleBase(x: int, y: int)

-        requires x > y;

-        ensures elems = {x y};

-  ------------------------------------------

-      - searching for an instance      ... OK 

-      - adding unification y <--> 743

-      - adding unification x <--> 744

-      - adding unification x > y <--> true

-      - adding unification {x, y} <--> {743, 744}

-      - delegating to method calls     ...

-      - verifying synthesized solution ... 

-      ~~~ VERIFIED ~~~

-

-

-

-

-  [*] Analyzing constructor

-  ------------------------------------------

-      constructor SetNode.Triple(x: int, y: int, z: int)

-        requires x != y;

-        requires y != z;

-        requires z != x;

-        ensures elems = {x y z};

-  ------------------------------------------

-      - searching for an instance      ... OK 

-      - adding unification z <--> -224

-      - adding unification y <--> -225

-      - adding unification x <--> -452

-      - adding unification x != y && (y != z && z != x) <--> true

-      - adding unification x != y <--> true

-      - adding unification y != z && z != x <--> true

-      - adding unification y != z <--> true

-      - adding unification z != x <--> true

-      - adding unification {x, y, z} <--> {-452, -225, -224}

-      - delegating to method calls     ...

-      - verifying synthesized solution ... 

-      !!! NOT VERIFIED !!!

-      Strengthening the pre-condition

-          - candidate pre-condition: x < y && z > y

-          - delegating to method calls     ...

-          - substitution method found:

-            constructor SetNode.TripleBase(x: int, y: int, z: int)

-              requires x < y;

-              requires y < z;

-              ensures elems = {x y z};

-            Unifications: 

-              z -> z

-          - verifying partial solution ... VERIFIED

-          - substitution method found:

-            constructor SetNode.TripleBase(x: int, y: int, z: int)

-              requires x < y;

-              requires y < z;

-              ensures elems = {x y z};

-            Unifications: 

-              z -> z

-        [*] Analyzing constructor

-        ------------------------------------------

-            constructor SetNode.Triple(x: int, y: int, z: int)

-              requires x != y;

-              requires y != z;

-              requires z != x;

-              requires !(x < y && z > y);

-              ensures elems = {x y z};

-        ------------------------------------------

-            - searching for an instance      ... OK 

-            - adding unification z <--> -484

-            - adding unification y <--> 123

-            - adding unification x <--> 122

-            - adding unification (x != y && (y != z && z != x)) && !(x < y && z > y) <--> true

-            - adding unification x != y && (y != z && z != x) <--> true

-            - adding unification x != y <--> true

-            - adding unification y != z && z != x <--> true

-            - adding unification y != z <--> true

-            - adding unification z != x <--> true

-            - adding unification !(x < y && z > y) <--> true

-            - adding unification x < y && z > y <--> false

-            - adding unification x < y <--> true

-            - adding unification z > y <--> false

-            - adding unification {x, y, z} <--> {-484, 122, 123}

-            - delegating to method calls     ...

-            - verifying synthesized solution ... 

-            !!! NOT VERIFIED !!!

-            Strengthening the pre-condition

-                - candidate pre-condition: z < x && y > x

-                - delegating to method calls     ...

-                - substitution method found:

-                  constructor SetNode.TripleBase(x: int, y: int, z: int)

-                    requires x < y;

-                    requires y < z;

-                    ensures elems = {x y z};

-                  Unifications: 

-                    z -> y

-                - verifying partial solution ... VERIFIED

-                - substitution method found:

-                  constructor SetNode.TripleBase(x: int, y: int, z: int)

-                    requires x < y;

-                    requires y < z;

-                    ensures elems = {x y z};

-                  Unifications: 

-                    z -> y

-              [*] Analyzing constructor

-              ------------------------------------------

-                  constructor SetNode.Triple(x: int, y: int, z: int)

-                    requires x != y;

-                    requires y != z;

-                    requires z != x;

-                    requires !(x < y && z > y);

-                    requires !(z < x && y > x);

-                    ensures elems = {x y z};

-              ------------------------------------------

-                  - searching for an instance      ... OK 

-                  - adding unification z <--> -853

-                  - adding unification y <--> -852

-                  - adding unification x <--> -854

-                  - adding unification ((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x) <--> true

-                  - adding unification (x != y && (y != z && z != x)) && !(x < y && z > y) <--> true

-                  - adding unification x != y && (y != z && z != x) <--> true

-                  - adding unification x != y <--> true

-                  - adding unification y != z && z != x <--> true

-                  - adding unification y != z <--> true

-                  - adding unification z != x <--> true

-                  - adding unification !(x < y && z > y) <--> true

-                  - adding unification x < y && z > y <--> false

-                  - adding unification x < y <--> true

-                  - adding unification z > y <--> false

-                  - adding unification !(z < x && y > x) <--> true

-                  - adding unification z < x && y > x <--> false

-                  - adding unification z < x <--> false

-                  - adding unification y > x <--> true

-                  - adding unification {x, y, z} <--> {-854, -853, -852}

-                  - delegating to method calls     ...

-                  - verifying synthesized solution ... 

-                  !!! NOT VERIFIED !!!

-                  Strengthening the pre-condition

-                      - candidate pre-condition: x < z && y > z

-                      - delegating to method calls     ...

-                      - substitution method found:

-                        constructor SetNode.TripleBase(x: int, y: int, z: int)

-                          requires x < y;

-                          requires y < z;

-                          ensures elems = {x y z};

-                        Unifications: 

-                          z -> y

-                      - verifying partial solution ... VERIFIED

-                      - substitution method found:

-                        constructor SetNode.TripleBase(x: int, y: int, z: int)

-                          requires x < y;

-                          requires y < z;

-                          ensures elems = {x y z};

-                        Unifications: 

-                          z -> y

-                    [*] Analyzing constructor

-                    ------------------------------------------

-                        constructor SetNode.Triple(x: int, y: int, z: int)

-                          requires x != y;

-                          requires y != z;

-                          requires z != x;

-                          requires !(x < y && z > y);

-                          requires !(z < x && y > x);

-                          requires !(x < z && y > z);

-                          ensures elems = {x y z};

-                    ------------------------------------------

-                        - searching for an instance      ... OK 

-                        - adding unification z <--> -303

-                        - adding unification y <--> -155

-                        - adding unification x <--> -154

-                        - adding unification (((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x)) && !(x < z && y > z) <--> true

-                        - adding unification ((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x) <--> true

-                        - adding unification (x != y && (y != z && z != x)) && !(x < y && z > y) <--> true

-                        - adding unification x != y && (y != z && z != x) <--> true

-                        - adding unification x != y <--> true

-                        - adding unification y != z && z != x <--> true

-                        - adding unification y != z <--> true

-                        - adding unification z != x <--> true

-                        - adding unification !(x < y && z > y) <--> true

-                        - adding unification x < y && z > y <--> false

-                        - adding unification x < y <--> false

-                        - adding unification z > y <--> false

-                        - adding unification !(z < x && y > x) <--> true

-                        - adding unification z < x && y > x <--> false

-                        - adding unification z < x <--> true

-                        - adding unification y > x <--> false

-                        - adding unification !(x < z && y > z) <--> true

-                        - adding unification x < z && y > z <--> false

-                        - adding unification x < z <--> false

-                        - adding unification y > z <--> true

-                        - adding unification {x, y, z} <--> {-303, -155, -154}

-                        - delegating to method calls     ...

-                        - verifying synthesized solution ... 

-                        !!! NOT VERIFIED !!!

-                        Strengthening the pre-condition

-                            - candidate pre-condition: z < y && x > y

-                            - delegating to method calls     ...

-                            - substitution method found:

-                              constructor SetNode.TripleBase(x: int, y: int, z: int)

-                                requires x < y;

-                                requires y < z;

-                                ensures elems = {x y z};

-                              Unifications: 

-                                z -> x

-                            - verifying partial solution ... VERIFIED

-                            - substitution method found:

-                              constructor SetNode.TripleBase(x: int, y: int, z: int)

-                                requires x < y;

-                                requires y < z;

-                                ensures elems = {x y z};

-                              Unifications: 

-                                z -> x

-                          [*] Analyzing constructor

-                          ------------------------------------------

-                              constructor SetNode.Triple(x: int, y: int, z: int)

-                                requires x != y;

-                                requires y != z;

-                                requires z != x;

-                                requires !(x < y && z > y);

-                                requires !(z < x && y > x);

-                                requires !(x < z && y > z);

-                                requires !(z < y && x > y);

-                                ensures elems = {x y z};

-                          ------------------------------------------

-                              - searching for an instance      ... OK 

-                              - adding unification z <--> -226

-                              - adding unification y <--> -227

-                              - adding unification x <--> -225

-                              - adding unification ((((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x)) && !(x < z && y > z)) && !(z < y && x > y) <--> true

-                              - adding unification (((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x)) && !(x < z && y > z) <--> true

-                              - adding unification ((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x) <--> true

-                              - adding unification (x != y && (y != z && z != x)) && !(x < y && z > y) <--> true

-                              - adding unification x != y && (y != z && z != x) <--> true

-                              - adding unification x != y <--> true

-                              - adding unification y != z && z != x <--> true

-                              - adding unification y != z <--> true

-                              - adding unification z != x <--> true

-                              - adding unification !(x < y && z > y) <--> true

-                              - adding unification x < y && z > y <--> false

-                              - adding unification x < y <--> false

-                              - adding unification z > y <--> true

-                              - adding unification !(z < x && y > x) <--> true

-                              - adding unification z < x && y > x <--> false

-                              - adding unification z < x <--> true

-                              - adding unification y > x <--> false

-                              - adding unification !(x < z && y > z) <--> true

-                              - adding unification x < z && y > z <--> false

-                              - adding unification x < z <--> false

-                              - adding unification y > z <--> false

-                              - adding unification !(z < y && x > y) <--> true

-                              - adding unification z < y && x > y <--> false

-                              - adding unification z < y <--> false

-                              - adding unification x > y <--> true

-                              - adding unification {x, y, z} <--> {-227, -226, -225}

-                              - delegating to method calls     ...

-                              - verifying synthesized solution ... 

-                              !!! NOT VERIFIED !!!

-                              Strengthening the pre-condition

-                                  - candidate pre-condition: y < z && x > z

-                                  - delegating to method calls     ...

-                                  - substitution method found:

-                                    constructor SetNode.TripleBase(x: int, y: int, z: int)

-                                      requires x < y;

-                                      requires y < z;

-                                      ensures elems = {x y z};

-                                    Unifications: 

-                                      z -> x

-                                  - verifying partial solution ... VERIFIED

-                                  - substitution method found:

-                                    constructor SetNode.TripleBase(x: int, y: int, z: int)

-                                      requires x < y;

-                                      requires y < z;

-                                      ensures elems = {x y z};

-                                    Unifications: 

-                                      z -> x

-                                [*] Analyzing constructor

-                                ------------------------------------------

-                                    constructor SetNode.Triple(x: int, y: int, z: int)

-                                      requires x != y;

-                                      requires y != z;

-                                      requires z != x;

-                                      requires !(x < y && z > y);

-                                      requires !(z < x && y > x);

-                                      requires !(x < z && y > z);

-                                      requires !(z < y && x > y);

-                                      requires !(y < z && x > z);

-                                      ensures elems = {x y z};

-                                ------------------------------------------

-                                    - searching for an instance      ... OK 

-                                    - adding unification z <--> 123

-                                    - adding unification y <--> -203

-                                    - adding unification x <--> 122

-                                    - adding unification (((((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x)) && !(x < z && y > z)) && !(z < y && x > y)) && !(y < z && x > z) <--> true

-                                    - adding unification ((((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x)) && !(x < z && y > z)) && !(z < y && x > y) <--> true

-                                    - adding unification (((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x)) && !(x < z && y > z) <--> true

-                                    - adding unification ((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x) <--> true

-                                    - adding unification (x != y && (y != z && z != x)) && !(x < y && z > y) <--> true

-                                    - adding unification x != y && (y != z && z != x) <--> true

-                                    - adding unification x != y <--> true

-                                    - adding unification y != z && z != x <--> true

-                                    - adding unification y != z <--> true

-                                    - adding unification z != x <--> true

-                                    - adding unification !(x < y && z > y) <--> true

-                                    - adding unification x < y && z > y <--> false

-                                    - adding unification x < y <--> false

-                                    - adding unification z > y <--> true

-                                    - adding unification !(z < x && y > x) <--> true

-                                    - adding unification z < x && y > x <--> false

-                                    - adding unification z < x <--> false

-                                    - adding unification y > x <--> false

-                                    - adding unification !(x < z && y > z) <--> true

-                                    - adding unification x < z && y > z <--> false

-                                    - adding unification x < z <--> true

-                                    - adding unification y > z <--> false

-                                    - adding unification !(z < y && x > y) <--> true

-                                    - adding unification z < y && x > y <--> false

-                                    - adding unification z < y <--> false

-                                    - adding unification x > y <--> true

-                                    - adding unification !(y < z && x > z) <--> true

-                                    - adding unification y < z && x > z <--> false

-                                    - adding unification y < z <--> true

-                                    - adding unification x > z <--> false

-                                    - adding unification {x, y, z} <--> {-203, 122, 123}

-                                    - delegating to method calls     ...

-                                    - verifying synthesized solution ... 

-                                    ~~~ VERIFIED ~~~

-  [*] Analyzing constructor

-  ------------------------------------------

-      constructor SetNode.TripleBase(x: int, y: int, z: int)

-        requires x < y;

-        requires y < z;

-        ensures elems = {x y z};

-  ------------------------------------------

-      - searching for an instance      ... OK 

-      - adding unification z <--> 596

-      - adding unification y <--> -384

-      - adding unification x <--> -385

-      - adding unification x < y && y < z <--> true

-      - adding unification x < y <--> true

-      - adding unification y < z <--> true

-      - adding unification {x, y, z} <--> {-385, -384, 596}

-      - delegating to method calls     ...

-      - verifying synthesized solution ... 

-      ~~~ VERIFIED ~~~

-

-

-Printing synthesized code

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index c6b8e493..f0e325e8 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -353,7 +353,7 @@ namespace Microsoft.Boogie {
     public bool PrintInlined = false;

     public bool ExtractLoops = false;

     public int LazyInlining = 0;

-    public int ProcedureCopyBound = 1;

+    public int ProcedureCopyBound = 0;

     public int StratifiedInlining = 0;

     public int StratifiedInliningOption = 0;

     public bool UseUnsatCoreForInlining = false;

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index da9e8faa..9b90b12a 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -152,11 +152,6 @@ namespace Microsoft.Boogie.SMTLib
       options.AddWeakSmtOption("TYPE_CHECK", "true");

       options.AddWeakSmtOption("BV_REFLECT", "true");

 

-      if (CommandLineOptions.Clo.LazyInlining == 2) {

-        options.AddWeakSmtOption("MACRO_EXPANSION", "true");

-        options.AddWeakSmtOption("WARNING", "false");

-      }

-

       if (options.TimeLimit > 0) {

         options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());

         options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);

diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 640f98ae..8929e732 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -84,9 +84,6 @@ namespace Microsoft.Boogie.Z3
       StringBuilder cmdLineArgsBldr = new StringBuilder();

       AppendCmdLineOption(cmdLineArgsBldr, "si");

 

-      if (CommandLineOptions.Clo.LazyInlining == 2) 

-        AppendCmdLineOption(cmdLineArgsBldr, "nw");

-

       if (CommandLineOptions.Clo.z3AtFlag)

         AppendCmdLineOption(cmdLineArgsBldr, "@");

 

@@ -165,9 +162,6 @@ namespace Microsoft.Boogie.Z3
             AddOption(result, "BV_REFLECT", "true");

       }

 

-      if (CommandLineOptions.Clo.LazyInlining == 2)

-        AddOption(result, "MACRO_EXPANSION", "true");

-      

       foreach (string opt in CommandLineOptions.Clo.Z3Options) {

         Contract.Assert(opt != null);

         int eq = opt.IndexOf("=");

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 576ce080..79fdaaa2 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -27,7 +27,6 @@ namespace VC {
     [NotDelayed]

     public VCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)

       : base(program)

-      // throws ProverException

     {

       Contract.Requires(program != null);

       this.appendLogFile = appendLogFile;

@@ -36,10 +35,6 @@ namespace VC {
 

       if (CommandLineOptions.Clo.LazyInlining > 0) {

         this.GenerateVCsForLazyInlining(program);

-        if (CommandLineOptions.Clo.LazyInlining == 3)

-        {

-            CreateCopiesForLazyInlining(CommandLineOptions.Clo.ProcedureCopyBound, program);

-        }

       }

     }

 

@@ -85,9 +80,9 @@ namespace VC {
       public Function function;

       public Variable controlFlowVariable;

       public List<Variable> interfaceVars;

+      public List<List<Variable>> interfaceVarCopies;

       public Expr assertExpr;

       public VCExpr vcexpr;

-      public VCExpr inside_vc; // (without the quantifiers)

       public List<VCExprVar> privateVars;

       public Dictionary<Incarnation, Absy> incarnationOriginMap;

       public Hashtable /*Variable->Expr*/ exitIncarnationMap;

@@ -163,6 +158,17 @@ namespace VC {
         Contract.Assert(returnVar != null);

         this.function = new Function(Token.NoToken, proc.Name, functionInterfaceVars, returnVar);

         ctxt.DeclareFunction(this.function, "");

+

+        interfaceVarCopies = new List<List<Variable>>();

+        int temp = 0;

+        for (int i = 0; i < CommandLineOptions.Clo.ProcedureCopyBound; i++) {

+          interfaceVarCopies.Add(new List<Variable>());

+          foreach (Variable v in interfaceVars) {

+            Constant constant = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, v.Name + temp++, v.TypedIdent.Type));

+            interfaceVarCopies[i].Add(constant);

+            //program.TopLevelDeclarations.Add(constant);

+          }

+        }

       }

     }

     [ContractInvariantMethod]

@@ -217,6 +223,25 @@ namespace VC {
           }

           Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(info.function), exprs);

           proc.Ensures.Add(new Ensures(true, freePostExpr));

+

+          if (CommandLineOptions.Clo.ProcedureCopyBound > 0) {

+            Expr ret = new LiteralExpr(Token.NoToken, false);

+            for (int k = 0; k < CommandLineOptions.Clo.ProcedureCopyBound; k++) {

+              var iv = info.interfaceVarCopies[k];

+              Contract.Assert(info.function.InParams.Length == iv.Count);

+

+              Expr conj = new LiteralExpr(Token.NoToken, true);

+              for (int i = 0; i < iv.Count; i++) {

+                Expr eqExpr = new NAryExpr(

+                  Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Eq), new ExprSeq(exprs[i], Expr.Ident(iv[i])));

+                conj =

+                  new NAryExpr(Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.And), new ExprSeq(conj, eqExpr));

+              }

+              ret =

+                new NAryExpr(Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Or), new ExprSeq(ret, conj));

+            }

+            proc.Ensures.Add(new Ensures(true, ret));

+          }

         }

       }

 

@@ -226,145 +251,6 @@ namespace VC {
       }

     }

 

-    // proc name -> k -> interface variables

-    public static Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies;

-    // proc name -> k -> VCExpr

-    Dictionary<string, List<VCExpr>> procVcCopies;

-

-    private void CreateCopiesForLazyInlining(int K, Program program)

-    {

-        interfaceVarCopies = new Dictionary<string, List<List<VCExprVar>>>();

-        procVcCopies = new Dictionary<string, List<VCExpr>>();

-

-        // Duplicate VCs of each procedure K times and remove quantifiers

-        Checker checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime);

-        foreach (LazyInliningInfo info in implName2LazyInliningInfo.Values)

-        {

-            Contract.Assert(info != null);

-            CreateCopyForLazyInlining(K, program, info, checker);

-        }

-

-        // Change the procedure calls in each VC

-        // Push all to the theorem prover

-        var bm = new BoundingVCMutator(checker.VCExprGen, interfaceVarCopies);

-        foreach (var kvp in procVcCopies)

-        {

-            for (int i = 0; i < kvp.Value.Count; i++)

-            {

-                kvp.Value[i] = bm.Mutate(kvp.Value[i], true);

-                checker.TheoremProver.PushVCExpression(kvp.Value[i]);

-            }

-        }

-    }

-

-    public class BoundingVCMutator : MutatingVCExprVisitor<bool>

-    {

-        // proc name -> k -> interface variables

-        Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies;

-

-        public BoundingVCMutator(VCExpressionGenerator gen, Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies)

-            : base(gen)

-        {

-            Contract.Requires(gen != null);

-            this.interfaceVarCopies = interfaceVarCopies;

-        }

-

-        protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,

-                                                      List<VCExpr/*!*/>/*!*/ newSubExprs,

-            // has any of the subexpressions changed?

-                                                      bool changed,

-                                                      bool arg)

-        {

-            //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null);

-            Contract.Ensures(Contract.Result<VCExpr>() != null);

-            

-            VCExpr node;

-            if (changed)

-                node = Gen.Function(originalNode.Op,

-                                   newSubExprs, originalNode.TypeArguments);

-            else

-                node = originalNode;

-

-            var expr = node as VCExprNAry;

-            if (expr == null) return node;

-            var op = expr.Op as VCExprBoogieFunctionOp;

-            if (op == null) return node;

-            if (!interfaceVarCopies.ContainsKey(op.Func.Name)) return node;

-

-            // substitute

-            var K = interfaceVarCopies[op.Func.Name].Count;

-            

-

-            VCExpr ret = VCExpressionGenerator.False;

-            for (int k = 0; k < K; k++)

-            {

-                var iv = interfaceVarCopies[op.Func.Name][k];

-                Contract.Assert(op.Arity == iv.Count);

-

-                VCExpr conj = VCExpressionGenerator.True;

-                for (int i = 0; i < iv.Count; i++)

-                {

-                    var c = Gen.Eq(expr[i], iv[i]);

-                    conj = Gen.And(conj, c);

-                }

-                ret = Gen.Or(conj, ret);

-            }

-

-            return ret;

-        }

-

-    } // end BoundingVCMutator

-

-    private static int newVarCnt = 0;

-

-    private void CreateCopyForLazyInlining(int K, Program program, LazyInliningInfo info, Checker checker) 

-    {

-        var translator = checker.TheoremProver.Context.BoogieExprTranslator;

-        interfaceVarCopies.Add(info.impl.Name, new List<List<VCExprVar>>());

-        procVcCopies.Add(info.impl.Name, new List<VCExpr>());

-

-        for (int k = 0; k < K; k++)

-        {

-            var expr = info.inside_vc;

-            // Instantiate the "forall" variables

-            Dictionary<VCExprVar, VCExpr> substForallDict = new Dictionary<VCExprVar, VCExpr>();

-            var ls = new List<VCExprVar>();

-            for (int i = 0; i < info.interfaceVars.Count; i++)

-            {

-                var v = translator.LookupVariable(info.interfaceVars[i]);

-                string newName = v.Name + "_fa_" + k.ToString() + "_" + newVarCnt.ToString();

-                newVarCnt++;

-                //checker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);

-                var vp = checker.VCExprGen.Variable(newName, v.Type);

-                substForallDict.Add(v, vp);

-                ls.Add(vp);

-            }

-            interfaceVarCopies[info.impl.Name].Add(ls);

-            VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());

-

-            SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(checker.VCExprGen);

-            Contract.Assert(subst != null);

-            expr = subst.Mutate(expr, substForall);

-

-            // Instantiate and declare the "exists" variables

-            Dictionary<VCExprVar, VCExpr> substExistsDict = new Dictionary<VCExprVar, VCExpr>();

-            foreach (VCExprVar v in info.privateVars)

-            {

-                Contract.Assert(v != null);

-                string newName = v.Name + "_te_" + k.ToString() + "_" + newVarCnt.ToString();

-                newVarCnt++;

-                checker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);

-                substExistsDict.Add(v, checker.VCExprGen.Variable(newName, v.Type));

-            }

-            VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());

-

-            subst = new SubstitutingVCExprVisitor(checker.VCExprGen);

-            expr = subst.Mutate(expr, substExists);

-

-            procVcCopies[info.impl.Name].Add(expr);

-        }

-    }

-

     private void GenerateVCForLazyInlining(Program program, LazyInliningInfo info, Checker checker) {

       Contract.Requires(program != null);

       Contract.Requires(info != null);

@@ -389,7 +275,7 @@ namespace VC {
       ResetPredecessors(impl.Blocks);

       VCExpr reachvcexpr = GenerateReachVC(impl, info, checker);

       vcexpr = gen.And(vcexpr, reachvcexpr);

-      

+

       List<VCExprVar> privateVars = new List<VCExprVar>();

       foreach (Variable v in impl.LocVars) {

         Contract.Assert(v != null);

@@ -401,7 +287,6 @@ namespace VC {
       }

 

       info.privateVars = privateVars;

-      info.inside_vc = vcexpr;

 

       if (privateVars.Count > 0) {

         vcexpr = gen.Exists(new List<TypeVariable>(), privateVars, new List<VCTrigger>(),

@@ -421,12 +306,7 @@ namespace VC {
       Function function = cce.NonNull(info.function);

       VCExpr expr = gen.Function(function, interfaceExprs);

       Contract.Assert(expr != null);

-      if (CommandLineOptions.Clo.LazyInlining == 1) {

-        vcexpr = gen.Implies(expr, vcexpr);

-      } else {

-        //Contract.Assert(CommandLineOptions.Clo.LazyInlining == 2);

-        vcexpr = gen.Eq(expr, vcexpr);

-      }

+      vcexpr = gen.Implies(expr, vcexpr);

 

       List<VCTrigger> triggers = new List<VCTrigger>();

       List<VCExpr> exprs = new List<VCExpr>();

@@ -442,10 +322,7 @@ namespace VC {
                           new VCQuantifierInfos(impl.Name, QuantifierExpr.GetNextSkolemId(), false, q), vcexpr);

 

       info.vcexpr = vcexpr;

-      if (CommandLineOptions.Clo.LazyInlining != 3)

-      {

-          checker.TheoremProver.PushVCExpression(vcexpr);

-      }

+      checker.TheoremProver.PushVCExpression(vcexpr);

     }

 

     protected VCExpr GenerateReachVC(Implementation impl, LazyInliningInfo info, Checker ch) {

@@ -1662,12 +1539,6 @@ namespace VC {
         VCExpr vc = parent.GenerateVCAux(impl, null, label2absy, checker);

         Contract.Assert(vc != null);

 

-        if (CommandLineOptions.Clo.LazyInlining == 3)

-        {

-            var bm = new BoundingVCMutator(checker.VCExprGen, interfaceVarCopies);

-            vc = bm.Mutate(vc, true);

-        }

-

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {

           reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, parent.implName2LazyInliningInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program);

         } else {