Merge

26 files changed, 1279 insertions, 501 deletions

diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index 42add00c..a98fa057 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -8,8 +8,8 @@ open MethodUnifier
 open Modularizer

 open PipelineUtils

 open Options

-open Printer

 open Resolver

+open PrintUtils

 open DafnyPrinter

 open Utils

 

@@ -41,13 +41,16 @@ let GenMethodAnalysisCode comp m assertion =
   let ppre,ppost = GetMethodPrePost m 

   let pre = Desugar ppre

   let post = Desugar ppost

+  //let sigStr = PrintSig signature

+  let sigVars = 

+    match signature with

+    | Sig(ins,outs) ->

+        List.concat [ins; outs] |> List.fold (fun acc vd -> acc + (sprintf "    var %s;" (PrintVarDecl vd)) + newline) ""

   "  method " + methodName + "()" + newline +

   "    modifies this;" + newline +

   "  {" + newline + 

   // print signature as local variables

-  (match signature with

-    | Sig(ins,outs) ->

-        List.concat [ins; outs] |> List.fold (fun acc vd -> acc + (sprintf "    var %s;" (PrintVarDecl vd)) + newline) "") +

+  sigVars +

   "    // assume precondition" + newline +

   "    assume " + (PrintExpr 0 pre) + ";" + newline + 

   "    // assume invariant and postcondition" + newline + 

@@ -65,7 +68,7 @@ let rec MethodAnalysisPrinter onlyForThese assertion comp =
   match onlyForThese with

   | (c,m) :: rest when GetComponentName c = cname -> 

     match m with 

-    | Method(methodName, sign, pre, post, true) -> 

+    | Method(methodName, sign, pre, post, _) -> 

         (GenMethodAnalysisCode c m assertion) + newline +

         (MethodAnalysisPrinter rest assertion comp)

     | _ -> ""

@@ -73,23 +76,27 @@ let rec MethodAnalysisPrinter onlyForThese assertion comp =
   | [] -> ""

 

 let rec IsArgsOnly args expr = 

+  let __IsArgsOnlyLst elist = 

+    elist |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true

   match expr with                                                

-  | IntLiteral(_)                        -> true

-  | BoolLiteral(_)                       -> true

-  | Star                                 -> true

-  | ObjLiteral(id)                       -> true

+  | IntLiteral(_)

+  | BoolLiteral(_)

+  | BoxLiteral(_)

+  | Star        

+  | VarDeclExpr(_)

+  | ObjLiteral(_)                        -> true

   | VarLiteral(id)

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

-  | UnaryExpr(_,e)                       -> IsArgsOnly args e

-  | BinaryExpr(_,_,e1,e2)                -> (IsArgsOnly args e1) && (IsArgsOnly args e2)

-  | IteExpr(c,e1,e2)                     -> (IsArgsOnly args c) && (IsArgsOnly args e1) && (IsArgsOnly args e2)

-  | Dot(e,_)                             -> IsArgsOnly args e

-  | SelectExpr(e1, e2)                   -> (IsArgsOnly args e1) && (IsArgsOnly args e2)

-  | UpdateExpr(e1, e2, e3)               -> (IsArgsOnly args e1) && (IsArgsOnly args e2) && (IsArgsOnly args e3)

-  | SequenceExpr(exprs) | SetExpr(exprs) -> exprs |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true

-  | SeqLength(e)                         -> IsArgsOnly args e

+  | Dot(e,_)

+  | SeqLength(e)

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

+  | SelectExpr(e1, e2)

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

+  | IteExpr(e3, e1, e2)         

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

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

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

   | ForallExpr(vars,e)                   -> IsArgsOnly (List.concat [args; vars]) e

-  | MethodCall(rcv,_,aparams)            -> rcv :: aparams |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true

 

 let AddUnif indent e v unifMap =

   let idt = Indent indent

@@ -134,12 +141,11 @@ let GetUnificationsForMethod indent comp m heapInst =
   (* --- function body starts here --- *)

   match m with

   | Method(mName,Sig(ins, outs),pre,post,_) -> 

-      let args = List.concat [ins; outs]

+      let args = ins

       match args with 

       | [] -> Map.empty

       | _  -> let unifs = GetArgValueUnifications args

-              GetUnifications indent args heapInst unifs (BinaryAnd pre post)

-              

+              GetUnifications indent args heapInst unifs (BinaryAnd pre post)                 

   | _ -> failwith ("not a method: " + m.ToString())

 

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

@@ -167,7 +173,8 @@ let GetObjRefExpr objRefName (heapInst: HeapInstance) =
                 | Some(expr) -> Some(Dot(expr, fldName))

                 | None -> __fff rest

             | [] -> None

-          let backPointers = heapInst.assignments |> List.filter (fun ((_,_),l) -> l = ObjLiteral(objRefName))

+          let backPointers = heapInst.assignments |> List.choose (function FieldAssignment (x,l) -> if l = ObjLiteral(objRefName) then Some(x,l) else None

+                                                                           |_ -> None)

           __fff backPointers 

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

   if objRef2ExprCache.ContainsKey(objRefName) then

@@ -187,13 +194,17 @@ let GetObjRefExpr objRefName (heapInst: HeapInstance) =
 //  =======================================================

 let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative = 

   let idt = Indent indent

+  /// 

   let __CheckUnif o f e idx =

     if not conservative || not Options.CONFIG.checkUnifications then 

       true 

     else

-      let objRefExpr = GetObjRefExpr o heapInst |> Utils.ExtractOptionMsg ("Couldn't find a path from 'this' to " + o)

-      let fldName = PrintVarName f                             

-      let lhs = Dot(objRefExpr, fldName)

+      let lhs = if o = NoObj then

+                  VarLiteral(GetVarName f)

+                else

+                  let objRefExpr = GetObjRefExpr o.name heapInst |> Utils.ExtractOptionMsg ("Couldn't find a path from 'this' to " + o.name)

+                  let fldName = GetVarName f                             

+                  Dot(objRefExpr, fldName)

       let assertionExpr = match f with

                           | Var(_, Some(SeqType(_))) when not (idx = -1) -> BinaryEq (SelectExpr(lhs, IntLiteral(idx))) e

                           | Var(_, Some(SetType(_))) when not (idx = -1) -> BinaryIn e lhs

@@ -207,43 +218,54 @@ let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative =
       else

         Logger.DebugLine " DOESN'T HOLD"

       ok

+  ///

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

+    if value = Const2Expr c then

+      if __CheckUnif o f e -1 then                                                

+        // change the value to expression

+        //Logger.TraceLine (sprintf "%s    - applied: %s.%s --> %s" idt (PrintConst o) (GetVarName f) (PrintExpr 0 e) )

+        e 

+      else

+        value

+    else 

+      let rec __UnifyOverLst lst cnt =

+        match lst with

+        | lstElem :: rest when lstElem = Const2Expr c ->

+            if __CheckUnif o f e cnt then

+              //Logger.TraceLine (sprintf "%s    - applied: %s.%s[%d] --> %s" idt (PrintConst o) (GetVarName f) cnt (PrintExpr 0 e) )

+              e :: __UnifyOverLst rest (cnt+1)

+            else  

+              lstElem :: __UnifyOverLst rest (cnt+1)

+        | lstElem :: rest ->

+            lstElem :: __UnifyOverLst rest (cnt+1)

+        | [] -> []

+      // see if it's a list, then try to match its elements, otherwise leave it as is

+      match value with

+      | SequenceExpr(elist) -> 

+          let newExprList = __UnifyOverLst elist 0

+          SequenceExpr(newExprList)

+      | SetExpr(elist) ->

+          let newExprList = __UnifyOverLst elist 0

+          SetExpr(newExprList)

+      | _ -> 

+          value

+

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

   match unifs with

   | (e,c) :: rest -> 

       let heapInst = ApplyUnifications indent prog comp mthd rest heapInst conservative

-      let newHeap = heapInst.assignments|> List.fold (fun acc ((o,f),value) ->

-                                                       if value = Const2Expr c then

-                                                         if __CheckUnif o.name f e -1 then                                                

-                                                           // change the value to expression

-                                                           //Logger.TraceLine (sprintf "%s    - applied: %s.%s --> %s" idt (PrintConst o) (GetVarName f) (PrintExpr 0 e) )

-                                                           Utils.ListMapAdd (o,f) e acc 

-                                                         else

-                                                           // don't change the value unless "conservative = false"

-                                                           Utils.ListMapAdd (o,f) value acc

-                                                       else 

-                                                         let rec __UnifyOverLst lst cnt =

-                                                               match lst with

-                                                               | lstElem :: rest when lstElem = Const2Expr c ->

-                                                                   if __CheckUnif o.name f e cnt then

-                                                                     //Logger.TraceLine (sprintf "%s    - applied: %s.%s[%d] --> %s" idt (PrintConst o) (GetVarName f) cnt (PrintExpr 0 e) )

-                                                                     e :: __UnifyOverLst rest (cnt+1)

-                                                                   else  

-                                                                     lstElem :: __UnifyOverLst rest (cnt+1)

-                                                               | lstElem :: rest ->

-                                                                   lstElem :: __UnifyOverLst rest (cnt+1)

-                                                               | [] -> []

-                                                         // see if it's a list, then try to match its elements, otherwise leave it as is

-                                                         match value with

-                                                         | SequenceExpr(elist) -> 

-                                                             let newExprList = __UnifyOverLst elist 0

-                                                             Utils.ListMapAdd (o,f) (SequenceExpr(newExprList)) acc

-                                                         | SetExpr(elist) ->

-                                                             let newExprList = __UnifyOverLst elist 0

-                                                             Utils.ListMapAdd (o,f) (SetExpr(newExprList)) acc

-                                                         | _ -> 

-                                                             Utils.ListMapAdd (o,f) value acc

-                                                     ) heapInst.assignments

-      {heapInst with assignments = newHeap }

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

+                                                        match asgn with

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

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

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

+                                                        | _ -> acc @ [asgn]

+                                                     ) [] 

+      let newRetVals = heapInst.methodRetVals |> Map.fold (fun acc key value ->

+                                                             let e2 = __Apply (NoObj,Var(key, None)) c e value

+                                                             acc |> Map.add key e2

+                                                          ) Map.empty

+      {heapInst with assignments = newHeap; methodRetVals = newRetVals}

   | [] -> heapInst

 

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

@@ -277,7 +299,10 @@ let GetHeapExpr prog mthd heapInst =
   //   - go through all objects on the heap and assert their invariants  

   let pre,post = GetMethodPrePost mthd

   let prepostExpr = post //TODO: do we need the "pre" here as well?

-  let heapObjs = heapInst.assignments |> List.fold (fun acc ((o,_),_) -> acc |> Set.add o) Set.empty

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

+                                                      match asgn with

+                                                      | FieldAssignment((o,_),_) -> acc |> Set.add o

+                                                      | _ -> acc) Set.empty

   heapObjs |> Set.fold (fun acc o -> 

                           let receiverOpt = GetObjRefExpr o.name heapInst

                           let receiver = Utils.ExtractOption receiverOpt

@@ -288,10 +313,10 @@ let GetHeapExpr prog mthd heapInst =
                       ) prepostExpr

 

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

-let FixSolution origMeth sol =

+let FixSolution origComp origMeth sol =

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

-                      if GetMethodName mm = GetMethodName origMeth then

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

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

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

                       else 

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

 

@@ -304,7 +329,7 @@ let rec AnalyzeConstructor indent prog comp m callGraph =
   let idt = Indent indent

   Logger.InfoLine (idt + "[*] Analyzing constructor")

   Logger.InfoLine (idt + "------------------------------------------")

-  Logger.InfoLine (PrintMethodSignFull (indent + 4) comp m)

+  Logger.InfoLine (Printer.PrintMethodSignFull (indent + 4) comp m)

   Logger.InfoLine (idt + "------------------------------------------")

   match TryFindExistingAndConvertToSolution indent comp m TrueLiteral callGraph with

   | Some(sol) -> sol

@@ -326,12 +351,12 @@ let rec AnalyzeConstructor indent prog comp m callGraph =
         Logger.InfoLine " OK "

         let model = models.[0]

         let hModel = ReadFieldValuesFromModel model prog comp m

-        let heapInst = ResolveModel hModel

+        let heapInst = ResolveModel hModel (GetMethodOutArgs m)

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

         let heapInst = ApplyUnifications indent prog comp m unifs heapInst true

         

         // split into method calls

-        let sol = MakeModular indent prog comp m TrueLiteral heapInst callGraph |> FixSolution m

+        let sol = MakeModular indent prog comp m TrueLiteral heapInst callGraph |> FixSolution comp m

 

         if Options.CONFIG.verifySolutions then

           Logger.InfoLine (idt + "    - verifying synthesized solution ... ")

@@ -353,9 +378,11 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph =
   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

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

   let expr = GetHeapExpr prog m heapInst2

   // now evaluate and see what's left

-  let newCond = Eval heapInst2 (function VarLiteral(_) -> false | _ -> true) expr

+  let newCond = Eval heapInst2 (function VarLiteral(id) when __IsMethodArg id -> false | _ -> true) expr

   if newCond = TrueLiteral then

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

     wrongSol

@@ -364,7 +391,7 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph =
       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 (GetMethodArgs m |> List.map (function Var(name,_) -> VarLiteral(name))) heapInst2

+        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 

@@ -385,11 +412,7 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph =
                     | None -> sol   

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

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

-//      let solRest = match FindExisting indent comp m3 (UnaryNot(candCond)) with

-//                    | Some(sol3) -> sol3

-//                    | None -> AnalyzeConstructor (indent + 2) prog comp m3

- 

-      MergeSolutions solThis solRest |> FixSolution m

+      MergeSolutions solThis solRest |> FixSolution comp m

     else 

       Logger.InfoLine "NOT VERIFIED"

       wrongSol  

@@ -398,7 +421,7 @@ let GetMethodsToAnalyze prog =
   let mOpt = Options.CONFIG.methodToSynth;

   if mOpt = "*" then

     (* all *)

-    FilterMembers prog FilterConstructorMembers

+    FilterMembers prog FilterMethodMembers // FilterConstructorMembers

   elif mOpt = "paramsOnly" then

     (* only with parameters *)

     FilterMembers prog FilterConstructorMembersWithParams 

@@ -408,7 +431,7 @@ let GetMethodsToAnalyze prog =
         mOpt.Substring(1), true

       else

         mOpt, false

-    (* exactly one *)

+    (* exact list *)

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

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

                                        let idx = m.LastIndexOf(".")

@@ -456,7 +479,7 @@ let rec AnalyzeMethods prog members solutionsSoFar =
   match members with

   | (comp,m) :: rest -> 

       match m with

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

+      | Method(_,_,_,_,_) -> 

           let sol = __AnalyzeConstructorDeep prog [comp,m] solutionsSoFar

           Logger.InfoLine ""

           AnalyzeMethods prog rest sol

diff --git a/Jennisys/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs
index ab3dc8bb..d0ad5310 100644
--- a/Jennisys/Jennisys/Ast.fs
+++ b/Jennisys/Jennisys/Ast.fs
@@ -31,6 +31,7 @@ type VarDecl =
 type Expr =

   | IntLiteral of int

   | BoolLiteral of bool

+  | BoxLiteral of string

   | VarLiteral of string  

   | IdLiteral of string 

   | ObjLiteral of string 

@@ -45,10 +46,13 @@ type Expr =
   | SeqLength of Expr

   | SetExpr of Expr list //TODO: maybe this should really be a set instead of a list

   | ForallExpr of VarDecl list * Expr

-  | MethodCall of (* receiver *) Expr * (* name *) string * (* actual parameters *) Expr list

+  | MethodCall of (* receiver *) Expr * (* component name *) string * (* method name *) string * (* actual parameters *) Expr list

+  | VarDeclExpr of (* var list *) VarDecl list * (* declareAlso *) bool

+

 type Const = 

   | IntConst   of int

   | BoolConst  of bool

+  | BoxConst   of string

   | SetConst   of Set<Const>

   | SeqConst   of Const list

   | NullConst

@@ -60,6 +64,7 @@ type Const =
 

 type Stmt =

   | Block of Stmt list

+  | ExprStmt of Expr

   | Assign of Expr * Expr

 

 type Signature =

diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index dc6534e1..8ac62606 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -20,10 +20,12 @@ let rec Rewrite rewriterFunc expr =
     | None -> Rewrite rewriterFunc e 

   match expr with

   | IntLiteral(_)

-  | BoolLiteral(_)                   

+  | BoolLiteral(_) 

+  | BoxLiteral(_)                  

   | Star      

   | VarLiteral(_) 

-  | ObjLiteral(_)                      

+  | ObjLiteral(_) 

+  | VarDeclExpr(_)                     

   | IdLiteral(_)                     -> match rewriterFunc expr with

                                         | Some(e) -> e

                                         | None -> expr

@@ -37,7 +39,7 @@ let rec Rewrite rewriterFunc expr =
   | UpdateExpr(e1,e2,e3)             -> UpdateExpr(__RewriteOrRecurse e1, __RewriteOrRecurse e2, __RewriteOrRecurse e3) 

   | SequenceExpr(exs)                -> SequenceExpr(exs |> List.map __RewriteOrRecurse)

   | SetExpr(exs)                     -> SetExpr(exs |> List.map __RewriteOrRecurse)

-  | MethodCall(rcv,name,aparams)     -> MethodCall(__RewriteOrRecurse rcv, name, aparams |> List.map __RewriteOrRecurse)

+  | MethodCall(rcv,cname,mname,ins)  -> MethodCall(__RewriteOrRecurse rcv, cname, mname, ins |> List.map __RewriteOrRecurse)

 

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

 /// Substitutes all occurences of all IdLiterals having 

@@ -50,7 +52,7 @@ let RewriteVars vars expr =
              match e with 

              | IdLiteral(id) when __IdIsArg id -> Some(VarLiteral(id))

              | _ -> None) expr

-

+  

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

 /// Substitutes all occurences of e1 with e2 in expr

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

@@ -93,10 +95,12 @@ let rec DescendExpr visitorFunc composeFunc leafVal expr =
     | fs :: rest -> rest |> List.fold (fun acc e -> composeFunc (composeFunc acc (visitorFunc e)) (DescendExpr visitorFunc composeFunc leafVal e)) (visitorFunc fs)

   match expr with

   | IntLiteral(_)

-  | BoolLiteral(_)                   

+  | BoolLiteral(_) 

+  | BoxLiteral(_)

   | Star      

   | VarLiteral(_) 

   | ObjLiteral(_)                      

+  | VarDeclExpr(_)

   | IdLiteral(_)                     -> leafVal

   | Dot(e, _)

   | ForallExpr(_,e)

@@ -106,7 +110,7 @@ let rec DescendExpr visitorFunc composeFunc leafVal expr =
   | BinaryExpr(_,_,e1,e2)            -> __Compose (e1 :: e2 :: [])

   | IteExpr(e1,e2,e3)                

   | UpdateExpr(e1,e2,e3)             -> __Compose (e1 :: e2 :: e3 :: [])

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

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

   | SequenceExpr(exs)                

   | SetExpr(exs)                     -> __Compose exs

               

@@ -115,10 +119,12 @@ let rec DescendExpr2 visitorFunc expr acc =
   let __Pipe elist = elist |> List.fold (fun a e -> a |> DescendExpr2 visitorFunc e) newAcc

   match expr with

   | IntLiteral(_)

-  | BoolLiteral(_)                   

+  | BoolLiteral(_)  

+  | BoxLiteral(_)                 

   | Star      

   | VarLiteral(_) 

-  | ObjLiteral(_)                      

+  | ObjLiteral(_)   

+  | VarDeclExpr(_)                   

   | IdLiteral(_)                     -> newAcc

   | Dot(e, _)

   | ForallExpr(_,e)

@@ -128,7 +134,7 @@ let rec DescendExpr2 visitorFunc expr acc =
   | BinaryExpr(_,_,e1,e2)            -> __Pipe (e1 :: e2 :: [])

   | IteExpr(e1,e2,e3)

   | UpdateExpr(e1,e2,e3)             -> __Pipe (e1 :: e2 :: e3 :: [])

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

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

   | SequenceExpr(exs)                

   | SetExpr(exs)                     -> __Pipe exs

 

@@ -233,6 +239,7 @@ let rec Const2Expr c =
   match c with

   | IntConst(n) -> IntLiteral(n)

   | BoolConst(b) -> BoolLiteral(b)

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

   | SeqConst(clist) -> 

       let expList = clist |> List.fold (fun acc c -> Const2Expr c :: acc) [] |> List.rev

       SequenceExpr(expList)

@@ -243,7 +250,7 @@ let rec Const2Expr c =
   | ThisConst(_,_) -> ObjLiteral("this")

   | NewObj(name,_) -> ObjLiteral(PrintGenSym name)

   | NullConst -> ObjLiteral("null")

-  | Unresolved(name) -> failwithf "don't want to convert unresolved(%s) to expr" name // IdLiteral(name) //

+  | Unresolved(id) -> BoxLiteral(id) // failwithf "don't want to convert Unresolved(%s) to expr" name // 

   | _ -> failwithf "not implemented or not supported: %O" c

 

 let rec Expr2Const e =

@@ -383,11 +390,21 @@ let GetSigVars sign =
   match sign with

   | Sig(ins, outs) -> List.concat [ins; outs]

 

-let GetMethodArgs mthd = 

+let GetMethodInArgs mthd = 

+  match mthd with

+  | Method(_,Sig(ins, _),_,_,_) -> ins

+  | _ -> failwith ("not a method: " + mthd.ToString())

+

+let GetMethodOutArgs mthd = 

   match mthd with

-  | Method(_,Sig(ins, outs),_,_,_) -> List.concat [ins; outs]

+  | Method(_,Sig(_, outs),_,_,_) -> outs

   | _ -> failwith ("not a method: " + mthd.ToString())

 

+let GetMethodArgs mthd = 

+  let ins = GetMethodInArgs mthd

+  let outs = GetMethodOutArgs mthd

+  List.concat [ins; outs]

+

 let rec GetTypeShortName ty =

   match ty with

   | IntType -> "int"

@@ -546,8 +563,10 @@ 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

   | VarLiteral(id) -> 

       try 

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

@@ -569,10 +588,10 @@ let rec __EvalSym resolverFunc ctx expr =
   | 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,name,aparams) ->

+  | 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', name, aparams')

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

   | SelectExpr(lst, idx) ->

       let lst' = __EvalSym resolverFunc ctx lst

       let idx' = __EvalSym resolverFunc ctx idx 

@@ -789,6 +808,8 @@ let MyDesugar expr removeOriginal =
     match expr with

     | IntLiteral(_)          

     | BoolLiteral(_)  

+    | BoxLiteral(_)

+    | VarDeclExpr(_)

     | IdLiteral(_)   

     | VarLiteral(_)        

     | ObjLiteral(_)

@@ -850,25 +871,34 @@ let ChangeThisReceiver receiver expr =
   let rec __ChangeThis locals expr = 

     match expr with

     | IntLiteral(_)

-    | BoolLiteral(_)                   

-    | Star                             

-    | VarLiteral(_)                    -> expr

-    | ObjLiteral("this")               -> receiver

-    | ObjLiteral(_)                    -> expr

-    | IdLiteral("null")                -> failwith "should never happen anymore"   //TODO

-    | IdLiteral("this")                -> failwith "should never happen anymore"

-    | IdLiteral(id)                    -> if Set.contains id locals then VarLiteral(id) else __ChangeThis locals (Dot(ObjLiteral("this"), id))

-    | Dot(e, id)                       -> Dot(__ChangeThis locals e, id)

-    | ForallExpr(vars,e)               -> let newLocals = vars |> List.map (function Var(name,_) -> name) |> Set.ofList |> Set.union locals

-                                          ForallExpr(vars, __ChangeThis newLocals e)   

-    | UnaryExpr(op,e)                  -> UnaryExpr(op, __ChangeThis locals e)

-    | SeqLength(e)                     -> SeqLength(__ChangeThis locals e)

-    | SelectExpr(e1, e2)               -> SelectExpr(__ChangeThis locals e1, __ChangeThis locals e2)

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

-    | IteExpr(e1,e2,e3)                -> IteExpr(__ChangeThis locals e1, __ChangeThis locals e2, __ChangeThis locals e3) 

-    | UpdateExpr(e1,e2,e3)             -> UpdateExpr(__ChangeThis locals e1, __ChangeThis locals e2, __ChangeThis locals e3) 

-    | SequenceExpr(exs)                -> SequenceExpr(exs |> List.map (__ChangeThis locals))

-    | SetExpr(exs)                     -> SetExpr(exs |> List.map (__ChangeThis locals))

-    | MethodCall(rcv,name,aparams)     -> MethodCall(__ChangeThis locals rcv, name, aparams |> List.map (__ChangeThis locals))

+    | BoolLiteral(_)       

+    | BoxLiteral(_)            

+    | Star   

+    | VarDeclExpr(_)                          

+    | VarLiteral(_)                        -> expr

+    | ObjLiteral("this")                   -> receiver

+    | ObjLiteral(_)                        -> expr

+    | IdLiteral("null")                    -> failwith "should never happen anymore"   //TODO

+    | IdLiteral("this")                    -> failwith "should never happen anymore"

+    | IdLiteral(id)                        -> if Set.contains id locals then VarLiteral(id) else __ChangeThis locals (Dot(ObjLiteral("this"), id))

+    | Dot(e, id)                           -> Dot(__ChangeThis locals e, id)

+    | ForallExpr(vars,e)                   -> let newLocals = vars |> List.map (function Var(name,_) -> name) |> Set.ofList |> Set.union locals

+                                              ForallExpr(vars, __ChangeThis newLocals e)   

+    | UnaryExpr(op,e)                      -> UnaryExpr(op, __ChangeThis locals e)

+    | SeqLength(e)                         -> SeqLength(__ChangeThis locals e)

+    | SelectExpr(e1, e2)                   -> SelectExpr(__ChangeThis locals e1, __ChangeThis locals e2)

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

+    | IteExpr(e1,e2,e3)                    -> IteExpr(__ChangeThis locals e1, __ChangeThis locals e2, __ChangeThis locals e3) 

+    | UpdateExpr(e1,e2,e3)                 -> UpdateExpr(__ChangeThis locals e1, __ChangeThis locals e2, __ChangeThis locals e3) 

+    | SequenceExpr(exs)                    -> SequenceExpr(exs |> List.map (__ChangeThis locals))

+    | SetExpr(exs)                         -> SetExpr(exs |> List.map (__ChangeThis locals))

+    | MethodCall(rcv,cname, mname,aparams) -> MethodCall(__ChangeThis locals rcv, cname, mname, aparams |> List.map (__ChangeThis locals))

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

   __ChangeThis Set.empty expr

+

+let rec ExtractTopLevelExpressions stmt = 

+  match stmt with

+  | ExprStmt(e)    -> [e]

+  | Assign(e1, e2) -> [e1; e2]

+  | Block(slist)   -> slist |> List.fold (fun acc s -> acc @ ExtractTopLevelExpressions s) [] 

+

diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs
index 85e1fd01..9c2dca77 100644
--- a/Jennisys/Jennisys/CodeGen.fs
+++ b/Jennisys/Jennisys/CodeGen.fs
@@ -3,9 +3,9 @@
 open Ast

 open AstUtils

 open Utils

-open Printer   

 open Resolver

 open TypeChecker

+open PrintUtils

 open DafnyPrinter

 open DafnyModelUtils

 

@@ -141,41 +141,58 @@ let PrintDafnyCodeSkeleton prog methodPrinterFunc genRepr =
         (sprintf "%s" (PrintValidFunctionCode comp prog genRepr)) + newline +

         // call the method printer function on all methods of this component

         (methodPrinterFunc comp) +

-        //(compMethods |> List.fold (fun acc m -> acc + (methodPrinterFunc comp m)) "") +

         // the end of the class

         "}" + newline + newline

       | _ -> assert false; "") ""

 

 let PrintAllocNewObjects heapInst indent = 

   let idt = Indent indent

-  heapInst.assignments |> List.fold (fun acc ((obj,fld),_) ->

-                                      if not (obj.name = "this") then

-                                        acc |> Set.add obj

-                                      else 

-                                        acc

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

+                                       match a with

+                                       | FieldAssignment((obj,fld),_) when not (obj.name = "this") ->

+                                           acc |> Set.add obj

+                                       | FieldAssignment(_, ObjLiteral(name)) when not (name = "this" || name = "null") ->

+                                           acc |> Set.add (heapInst.objs |> Map.find name)

+                                       | _ -> acc

                                    ) Set.empty

                        |> Set.fold (fun acc obj -> acc + (sprintf "%svar %s := new %s;%s" idt obj.name (PrintType obj.objType) newline)) ""

 

 let PrintVarAssignments heapInst indent = 

   let idt = Indent indent

-  heapInst.assignments |> List.fold (fun acc ((o,f),e) ->

-                                      let fldName = PrintVarName f

-                                      let exprStr = 

-                                        if fldName = "" then

-                                          sprintf "%s;" (PrintExpr 0 e)

-                                        else

-                                          let value = PrintExpr 0 e

-                                          sprintf "%s.%s := %s;" o.name fldName value

-                                      acc + idt + exprStr + newline

-                                    ) ""

+  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)

+  str + newline

 

+///

 let PrintReprAssignments prog heapInst indent = 

   let __FollowsFunc o1 o2 = 

-    heapInst.assignments |> List.fold (fun acc ((srcObj,fld),value) -> 

-                                        acc || (srcObj = o1 && value = ObjLiteral(o2.name))

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

+                                         match assgn with

+                                         | FieldAssignment ((srcObj,fld),value) -> acc || (srcObj = o1 && value = ObjLiteral(o2.name))

+                                         | _ -> false

                                       ) false

   let idt = Indent indent

-  let objs = heapInst.assignments |> List.fold (fun acc ((obj,(Var(fldName,_))),_) -> if fldName = "" then acc else acc |> Set.add obj) Set.empty

+  let objs = heapInst.assignments |> List.fold (fun acc assgn -> 

+                                                  match assgn with

+                                                  | FieldAssignment((obj,(Var(fldName,_))),_) -> if fldName = "" then acc else acc |> Set.add obj

+                                                  | _ -> acc

+                                               ) Set.empty

                                   |> Set.toList

                                   |> Utils.TopSort __FollowsFunc

                                   |> List.rev

@@ -187,20 +204,21 @@ let PrintReprAssignments prog heapInst indent =
                                             let! comp = FindComponent prog typeName

                                             let vars = GetFrameFields comp

                                             let nonNullVars = vars |> List.filter (fun v -> 

-                                                                                      match Utils.ListMapTryFind (obj,v) heapInst.assignments with

+                                                                                      let lst = heapInst.assignments |> List.choose (function FieldAssignment(x,y) -> Some(x,y) | _ -> None)

+                                                                                      match Utils.ListMapTryFind (obj,v) lst with

                                                                                       | Some(ObjLiteral(n)) when not (n = "null") -> true

                                                                                       | _ -> false)

                                             return nonNullVars |> List.fold (fun a v -> 

-                                                                               BinaryPlus a (Dot(Dot(ObjLiteral(obj.name), (PrintVarName v)), "Repr"))

+                                                                                BinaryPlus a (Dot(Dot(ObjLiteral(obj.name), (GetVarName v)), "Repr"))

                                                                             ) expr

                                           }

                                           let fullReprExpr = BinaryGets (Dot(ObjLiteral(obj.name), "Repr")) fullRhs 

                                           fullReprExpr :: acc

-                                       ) []

+                                        ) []

   

   if not (reprGetsList = []) then

     idt + "// repr stuff" + newline + 

-    (PrintStmtList reprGetsList indent)

+    (PrintStmtList reprGetsList indent true)

   else

     ""

                                                           

@@ -236,13 +254,24 @@ let rec PrintHeapCreationCode prog sol indent genRepr =
 let PrintPrePost pfix expr = 

   SplitIntoConjunts expr |> PrintSep "" (fun e -> pfix + (PrintExpr 0 e) + ";")

 

+let GetPreconditionForMethod m = 

+  let validExpr = IdLiteral("Valid()");

+  match m with

+  | Method(_,_,pre,_,isConstr) ->

+      if isConstr then

+        pre

+      else

+        BinaryAnd validExpr pre

+  | _ -> failwithf "expected a method, got %O" m     

+

 let GetPostconditionForMethod m genRepr = 

   let validExpr = IdLiteral("Valid()");

   match m with

-  | Method(_,_,_,post,_) ->

+  | Method(_,_,_,post,isConstr) ->

       let postExpr = BinaryAnd validExpr post

       if genRepr then

-        BinaryAnd (IdLiteral("fresh(Repr - {this})")) postExpr

+        let freshExpr = if isConstr then "fresh(Repr - {this})" else "fresh(Repr - old(Repr))";

+        BinaryAnd (IdLiteral(freshExpr)) postExpr

       else

         postExpr

   | _ -> failwithf "expected a method, got %O" m     

@@ -251,7 +280,7 @@ let GenConstructorCode mthd body genRepr =
   let validExpr = IdLiteral("Valid()");

   match mthd with

   | Method(methodName, sign, pre, post, _) -> 

-      let preExpr = pre |> Desugar

+      let preExpr = GetPreconditionForMethod mthd |> Desugar

       let postExpr = GetPostconditionForMethod mthd genRepr |> Desugar

       "  method " + methodName + (PrintSig sign) + newline +

       "    modifies this;" + 

diff --git a/Jennisys/Jennisys/DafnyPrinter.fs b/Jennisys/Jennisys/DafnyPrinter.fs
index 43536ceb..73b9415a 100644
--- a/Jennisys/Jennisys/DafnyPrinter.fs
+++ b/Jennisys/Jennisys/DafnyPrinter.fs
@@ -2,7 +2,7 @@
 

 open Ast

 open AstUtils

-open Printer

+open PrintUtils

 

 let rec PrintType ty =

   match ty with

@@ -13,14 +13,24 @@ let rec PrintType ty =
   | NamedType(id,args)        -> if List.isEmpty args then id else sprintf "%s<%s>" id (PrintSep ", " (fun s -> s) args)

   | InstantiatedType(id,args) -> sprintf "%s<%s>" id (PrintSep ", " (fun t -> PrintType t) args)

 

+let PrintVarDecl vd =

+  match vd with

+  | Var(id,None) -> id

+  | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty)

+

 let rec PrintExpr ctx expr =

   match expr with

   | IntLiteral(d)     -> sprintf "%d" d

   | BoolLiteral(b)    -> sprintf "%b" b

+  | BoxLiteral(id)    -> sprintf "box_%s" id

   | ObjLiteral(id)

   | VarLiteral(id)

   | IdLiteral(id) -> id

-  | Star -> assert false; "" // I hope this won't happen

+  | VarDeclExpr(vlist, declare) -> 

+      let decl = if declare then "var " else ""

+      let vars = PrintSep ", " PrintVarDecl vlist

+      sprintf "%s%s" decl vars

+  | Star -> "*"

   | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id

   | UnaryExpr(op,UnaryExpr(op2, e2))   -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))

   | UnaryExpr(op,e) -> sprintf "%s%s" op (PrintExpr 90 e)

@@ -54,13 +64,14 @@ let rec PrintExpr ctx expr =
       let openParen = if needParens then "(" else ""

       let closeParen = if needParens then ")" else ""

       sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen

-  | MethodCall(rcv, name, aparams) ->

+  | MethodCall(rcv,_,name,aparams) ->

       sprintf "%s.%s(%s)" (PrintExpr 0 rcv) name (aparams |> PrintSep ", " (PrintExpr 0))

 

 let rec PrintConst cst = 

   match cst with 

   | IntConst(v)        -> sprintf "%d" v

   | BoolConst(b)       -> sprintf "%b" b

+  | BoxConst(id)       -> sprintf "box_%s" id

   | VarConst(v)        -> sprintf "%s" v

   | SetConst(cset)     -> sprintf "{%s}" (PrintSep ", " (fun c -> PrintConst c) (Set.toList cset))

   | SeqConst(cseq)     -> sprintf "[%s]" (PrintSep ", " (fun c -> PrintConst c) cseq)

@@ -70,6 +81,14 @@ let rec PrintConst cst =
   | NewObj(name,_)     -> PrintGenSym name

   | Unresolved(name)   -> sprintf "Unresolved(%s)" name

 

+let PrintSig signature =

+  match signature with

+  | Sig(ins, outs) ->

+      let returnClause = 

+        if outs <> [] then sprintf " returns (%s)" (outs |> PrintSep ", " PrintVarDecl)

+        else ""

+      sprintf "(%s)%s" (ins |> PrintSep ", " PrintVarDecl) returnClause

+

 let PrintTypeParams typeParams = 

   match typeParams with

   | [] -> ""

@@ -81,13 +100,15 @@ let PrintFields vars indent ghost =
                                   | Var(nm,None)     -> acc + (sprintf "%s%svar %s;%s" (Indent indent) ghostStr nm newline)

                                   | Var(nm,Some(tp)) -> acc + (sprintf "%s%svar %s: %s;%s" (Indent indent) ghostStr nm (PrintType tp) newline)) ""

 

-let rec PrintStmt stmt indent =

-  let idt = (Indent indent)

+let rec PrintStmt stmt indent printNewline =

+  let idt = Indent indent

+  let nl = if printNewline then newline else ""

   match stmt with

   | Block(stmts) ->

-      idt + "{" + newline +

-      (PrintStmtList stmts (indent + 2)) +

-      idt + "}" + newline

-  | Assign(lhs,rhs) -> sprintf "%s%s := %s;%s" idt (PrintExpr 0 lhs) (PrintExpr 0 rhs) newline

-and PrintStmtList stmts indent =

-  stmts |> List.fold (fun acc s -> acc + (PrintStmt s indent)) ""
\ No newline at end of file
+      idt + "{" + nl +

+      (PrintStmtList stmts (indent + 2) true) +

+      idt + "}" + nl

+  | Assign(lhs,rhs) -> sprintf "%s%s := %s;%s" idt (PrintExpr 0 lhs) (PrintExpr 0 rhs) nl

+  | ExprStmt(expr) -> sprintf "%s%s;%s" idt (PrintExpr 0 expr) nl

+and PrintStmtList stmts indent printNewLine =

+  stmts |> List.fold (fun acc s -> acc + (PrintStmt s indent printNewLine)) ""
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index 37b943c6..b9ec91c6 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/Number.jen /method:Number.Abs /genRepr  /genMod</StartArguments>

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

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

   </PropertyGroup>

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

@@ -43,6 +43,7 @@
     <FsYaccOutputFolder>$(IntermediateOutputPath)</FsYaccOutputFolder>

   </PropertyGroup>

   <ItemGroup>

+    <Compile Include="SymGen.fs" />

     <Compile Include="Logger.fs" />

     <Compile Include="Utils.fs" />

     <Compile Include="Options.fs" />

@@ -65,6 +66,7 @@
     <FsLex Include="Lexer.fsl">

       <OtherFlags>--unicode</OtherFlags>

     </FsLex>

+    <Compile Include="PrintUtils.fs" />

     <Compile Include="Printer.fs" />

     <Compile Include="DafnyPrinter.fs" />

     <Compile Include="TypeChecker.fs" />

diff --git a/Jennisys/Jennisys/MethodUnifier.fs b/Jennisys/Jennisys/MethodUnifier.fs
index 0f675e4d..af59799e 100644
--- a/Jennisys/Jennisys/MethodUnifier.fs
+++ b/Jennisys/Jennisys/MethodUnifier.fs
@@ -2,7 +2,7 @@
 

 open Ast

 open AstUtils

-open Printer 

+open PrintUtils

 open Resolver

 open Utils

 

@@ -11,7 +11,29 @@ exception CannotUnify
 type UnifDirection = LTR | RTL

 

 let rec UnifyImplies lhs rhs dir unifs = 

-  let ___AddOrNone unifs name e = Some(unifs |> Utils.MapAddNew name e)

+  ///

+  let __AddOrNone unifs name e = Some(unifs |> Utils.MapAddNew name e)

+  ///

+  let __UnifLists lstL lstR = 

+    if List.length lstL = List.length lstR then

+      try 

+        let unifs2 = List.fold2 (fun acc elL elR -> match UnifyImplies elL elR dir acc with

+                                                    | Some(u) -> u

+                                                    | None -> raise CannotUnify) unifs lstL lstR

+        Some(unifs2)

+      with 

+      | CannotUnify -> None

+    else

+      None

+  ///

+  let __ApplyUnifs unifs exprList = 

+            exprList |> List.fold (fun acc e -> 

+                                     let e' = e |> Rewrite (fun e ->

+                                                              match e with 

+                                                              | VarLiteral(id) when Map.containsKey id unifs -> Some(unifs |> Map.find id)

+                                                              | _ -> None)

+                                     acc |> Set.add e'

+                                  ) Set.empty

 

   if lhs = FalseLiteral || rhs = TrueLiteral then

     Some(unifs)

@@ -21,17 +43,20 @@ let rec UnifyImplies lhs rhs dir unifs =
                 | LTR -> lhs,rhs

                 | RTL -> rhs,lhs

       match l, r with

-      | VarLiteral(vname), rhs -> ___AddOrNone unifs vname rhs

+      | VarLiteral(vname), rhs -> __AddOrNone unifs vname rhs

       | IntLiteral(nL), IntLiteral(nR) when nL = nR -> 

           Some(unifs)

       | BoolLiteral(bL), BoolLiteral(bR) when bL = bR -> 

           Some(unifs)

-      | SetExpr(elistL),  SetExpr(elistR) 

+      | SetExpr(elistL),  SetExpr(elistR) ->

+          let s1 = elistL |> __ApplyUnifs unifs 

+          let s2 = elistR |> Set.ofList

+          if (s1 = s2) then 

+            Some(unifs)

+          else

+            __UnifLists elistL elistR

       | SequenceExpr(elistL), SequenceExpr(elistR) when List.length elistL = List.length elistR ->

-          let unifs2 = List.fold2 (fun acc elL elR -> match UnifyImplies elL elR dir acc with

-                                                      | Some(u) -> u

-                                                      | None -> raise CannotUnify) unifs elistL elistR

-          Some(unifs2)

+          __UnifLists elistL elistR

       | _ when l = r ->

           Some(unifs)

       | _ ->

@@ -93,8 +118,10 @@ let rec UnifyImplies lhs rhs dir unifs =
                 // we've found unifications for all target expressions -> return the current unifications map

                 Some(unifs)

                   

-          let lhsConjs = lhs |> DesugarAndRemove |> DistributeNegation |> SplitIntoConjunts

-          let rhsConjs = rhs |> DesugarAndRemove |> DistributeNegation |> SplitIntoConjunts

+          let __HasSetExpr e = DescendExpr2 (fun ex acc -> if acc then true else match ex with SetExpr(_) -> true | _ -> false) e false

+          let __PreprocSplitSort e = e |> DesugarAndRemove |> DistributeNegation |> SplitIntoConjunts |> List.sortBy (fun e -> if __HasSetExpr e then 1 else 0)

+          let lhsConjs = lhs |> __PreprocSplitSort

+          let rhsConjs = rhs |> __PreprocSplitSort

           ___f1 rhsConjs lhsConjs unifs

     with

     | KeyAlreadyExists

@@ -131,11 +158,28 @@ let TryFindExisting comp targetMthd =
   | Some(m,unifs) -> m,unifs

   | None -> targetMthd, Map.empty

 

-let ApplyMethodUnifs m unifs =

-  GetMethodArgs m |> List.map (fun (Var(name,_)) -> 

-                                 match Map.tryFind name unifs with

-                                 | Some(e) -> e

-                                 | None -> VarLiteral(name))

+let ApplyMethodUnifs receiver (c,m) unifs =

+  let __Apply args = args |> List.map (fun (Var(name,_)) -> 

+                                             match Map.tryFind name unifs with

+                                             | Some(e) -> e

+                                             | None -> VarLiteral(name))

+  let ins = GetMethodInArgs m |> __Apply

+  let outs = GetMethodOutArgs m |> __Apply

+  

+  let retVars, asgs = outs |> List.fold (fun (acc1,acc2) e -> 

+                                          let vname = SymGen.NewSym

+                                          let v = Var(vname, None)

+                                          let acc1' = acc1 @ [v]

+                                          let acc2' = acc2 @ [ArbitraryStatement(Assign(VarLiteral(vname), e))]

+                                          acc1', acc2'

+                                       ) ([],[])

+  let mcallExpr = MethodCall(receiver, GetComponentName c, GetMethodName m, ins)

+  match retVars, outs with

+  | [], [] -> [ArbitraryStatement(ExprStmt(mcallExpr))]

+  | [_], [VarLiteral(vn2)] -> [ArbitraryStatement(Assign(VarDeclExpr([Var(vn2, None)], false), mcallExpr))]

+  | _ ->

+      let mcall = ArbitraryStatement(Assign(VarDeclExpr(retVars, true), mcallExpr))

+      mcall :: asgs

 

 let TryFindExistingAndConvertToSolution indent comp m cond callGraph =

   let __Calls caller callee =

@@ -155,14 +199,21 @@ let TryFindExistingAndConvertToSolution indent comp m cond callGraph =
     match TryFindAMatch m candidateMethods with

     | Some(m',unifs) -> 

         Logger.InfoLine (idt + "    - substitution method found:")

-        Logger.InfoLine (PrintMethodSignFull (indent+6) comp m')

-        let args = ApplyMethodUnifs m' unifs

-        let delegateCall = MethodCall(ThisLiteral, GetMethodName m', args)

+        Logger.InfoLine (Printer.PrintMethodSignFull (indent+6) comp m')

+        Logger.DebugLine (idt + "      Unifications: ")

+        let idtt = idt + "        "

+        unifs |> Map.fold (fun acc k v -> acc + (sprintf "%s%s -> %s%s" idtt k (Printer.PrintExpr 0 v) newline)) "" |> Logger.Debug 

+//        let ins,outs = ApplyMethodUnifs m' unifs

+//        let delegateCall = MethodCall(ThisLiteral, GetMethodName m', ins)

+//        let obj = { name = "this"; objType = GetClassType comp }

+//        let var = Var("", None)

+//        let body = [FieldAssignment((obj,var), delegateCall)]

         let obj = { name = "this"; objType = GetClassType comp }

-        let var = Var("", None)

-        let body = [(obj,var), delegateCall]

-        let hInst = { assignments = body; 

+        let body = ApplyMethodUnifs ThisLiteral (comp,m') unifs

+        let hInst = { objs        = Utils.MapSingleton obj.name obj;

+                      assignments = body; 

                       methodArgs  = Map.empty; 

+                      methodRetVals = Map.empty;

                       globals     = Map.empty }

         Some(Map.empty |> Map.add (comp,m) [cond, hInst]

                        |> Map.add (comp,m') [])

diff --git a/Jennisys/Jennisys/Modularizer.fs b/Jennisys/Jennisys/Modularizer.fs
index 9bb3da72..b196d4cb 100644
--- a/Jennisys/Jennisys/Modularizer.fs
+++ b/Jennisys/Jennisys/Modularizer.fs
@@ -3,7 +3,7 @@
 open Ast

 open AstUtils

 open MethodUnifier

-open Printer 

+open PrintUtils

 open Resolver

 open Utils

 

@@ -27,7 +27,10 @@ let MergeSolutions sol1 sol2 =
     | [] -> res

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

   __Merge sol1 (sol2 |> Map.toList) sol1 

-                   

+ 

+//  ===========================================                   

+///

+//  ===========================================                   

 let rec MakeModular indent prog comp meth cond hInst callGraph = 

   let rec __AddDirectChildren e acc = 

     match e with

@@ -37,7 +40,7 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
     | _ -> acc

 

   let __GetDirectChildren = 

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

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

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

                  |> Set.toList

 

@@ -54,7 +57,11 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
 

   let __FindObj objName = 

     try 

-      hInst.assignments |> List.find (fun ((obj,_),_) -> obj.name = objName) |> fst |> fst

+      //hInst.assignments |> List.find (fun ((obj,_),_) -> obj.name = objName) |> fst |> fst

+      hInst.assignments |> List.choose (function FieldAssignment((obj,_),_) -> 

+                                                   if (obj.name = objName) then Some(obj) else None 

+                                                 | _ -> None)

+                        |> List.head

     with

       | ex -> failwithf "obj %s not found for method %s" objName (GetMethodFullName comp meth)

 

@@ -66,11 +73,13 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
   /// assignments that correspond to abstract fields of the given "objLitName" object

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

   let __GetAbsFldAssignments objLitName = 

-    hInst.assignments |> List.choose (fun ((obj,var),e) ->

-                                        if obj.name = objLitName && __IsAbstractField obj.objType var then

-                                          Some(var,e)

-                                        else

-                                          None)

+    hInst.assignments |> List.choose (function

+                                        FieldAssignment ((obj,var),e) ->

+                                          if obj.name = objLitName && __IsAbstractField obj.objType var then

+                                            Some(var,e)

+                                          else

+                                            None

+                                        | _ -> None)

 

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

   /// The given assignment is: 

@@ -110,7 +119,9 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
   //  ================================================================================

   let __GetSpecFor objLitName =

     let absFieldAssignments = __GetAbsFldAssignments objLitName

-    absFieldAssignments |> List.fold (fun acc (Var(name,_),e) -> BinaryAnd acc (__ExamineAndFix (IdLiteral(name)) e)) TrueLiteral

+    let absFldAssgnExpr = absFieldAssignments |> List.fold (fun acc (Var(name,_),e) -> BinaryAnd acc (__ExamineAndFix (IdLiteral(name)) e)) TrueLiteral

+    let retValExpr = hInst.methodRetVals |> Map.fold (fun acc varName varValueExpr -> BinaryAnd acc (BinaryEq (VarLiteral(varName)) varValueExpr)) TrueLiteral

+    BinaryAnd absFldAssgnExpr retValExpr

   

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

   /// Simply traverses a given expression and returns all arguments of the "meth" method that are used

@@ -138,7 +149,7 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
         let m = Method(mName, sgn, pre, post, true)

         let c = FindComponent prog (name |> __GetObjLitType |> GetTypeShortName) |> Utils.ExtractOption

         let m',unifs = TryFindExisting c m

-        let args = ApplyMethodUnifs m' unifs

+        let args = ApplyMethodUnifs obj (c,m') unifs

         __GetDelegateMethods rest (acc |> Map.add obj (c,m',args))

     | _ :: rest -> failwith "internal error: expected to see only ObjLiterals"

     | [] -> acc

@@ -151,22 +162,17 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
   let __GetModularBranch = 

     let delegateMethods = __GetDelegateMethods (directChildren.Force()) Map.empty

     let initChildrenExprList = delegateMethods |> Map.toList

-                                                |> List.map (fun (receiver, (cmp,mthd,args)) -> 

-                                                              let key = __FindObj (PrintExpr 0 receiver), Var("", None)

-                                                              let e = MethodCall(receiver, GetMethodName mthd, args)

-                                                              (key, e))

-    let newAssgns = hInst.assignments |> List.filter (fun ((obj,_),_) -> if obj.name = "this" then true else false)

-    let newProg, newComp, newMethodsLst = delegateMethods |> Map.fold (fun acc receiver (c,newMthd,_) ->

-                                                                          let obj = __FindObj (PrintExpr 0 receiver)

-                                                                          match acc with

-                                                                          | accProg, accComp, accmList ->

-                                                                              let oldComp = FindComponent accProg (GetTypeShortName obj.objType) |> Utils.ExtractOption

-                                                                              let prog', mcomp' = AddReplaceMethod accProg oldComp newMthd None

-                                                                              let mList' = (mcomp', newMthd) :: accmList

-                                                                              let comp' = if accComp = oldComp then mcomp' else accComp

-                                                                              prog', comp', mList'

-                                                                      ) (prog, comp, [])

-    newProg, newComp, newMethodsLst, { hInst with assignments = initChildrenExprList @ newAssgns }

+                                               |> List.map (fun (_, (_,_,asgs)) -> asgs)

+                                               |> List.concat

+//TODO(remove)

+//                                                              let key = __FindObj (Printer.PrintExpr 0 receiver), Var("", None)

+//                                                              let e = MethodCall(receiver, GetMethodName mthd, fst args)

+//                                                              FieldAssignment(key, e))

+    let newAssgns = hInst.assignments |> List.filter (function FieldAssignment((obj,_),_) -> obj.name = "this" | _ -> false)

+    let newMethodsLst = delegateMethods |> Map.fold (fun acc receiver (c,newMthd,_) ->

+                                                       (c,newMthd) :: acc

+                                                    ) []

+    newMethodsLst, { hInst with assignments = initChildrenExprList @ newAssgns }

 

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

   let idt = Indent indent

@@ -181,7 +187,7 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
     | Some(sol) -> sol

     | None -> 

         // if not found, try to split into parts

-        let _, _, newMthdLst, newHeapInst = __GetModularBranch

+        let newMthdLst, newHeapInst = __GetModularBranch

         let msol = Utils.MapSingleton (comp,meth) [cond, newHeapInst]

         newMthdLst |> List.fold (fun acc (c,m) -> 

                                    acc |> MergeSolutions (Utils.MapSingleton (c,m) []) 

diff --git a/Jennisys/Jennisys/Parser.fsy b/Jennisys/Jennisys/Parser.fsy
index e854d749..2dd1eb35 100644
--- a/Jennisys/Jennisys/Parser.fsy
+++ b/Jennisys/Jennisys/Parser.fsy
@@ -91,7 +91,7 @@ BlockStmt:
 Member:

     | VAR VarDecl                            { Field($2) }

     | CONSTRUCTOR ID Signature Pre Post      { Method($2, $3, RewriteVars (GetSigVars $3) $4, RewriteVars (GetSigVars $3) $5, true) }

-    | METHOD ID Signature Pre Post           { Method($2, $3, $4, $5, false) }

+    | METHOD ID Signature Pre Post           { Method($2, $3, RewriteVars (GetSigVars $3) $4, RewriteVars (GetSigVars $3) $5, false) }

 	  | INVARIANT ExprList                     { Invariant($2) }

 

 FrameMembers:

diff --git a/Jennisys/Jennisys/PrintUtils.fs b/Jennisys/Jennisys/PrintUtils.fs
new file mode 100644
index 00000000..138b5e77
--- /dev/null
+++ b/Jennisys/Jennisys/PrintUtils.fs
@@ -0,0 +1,12 @@
+module PrintUtils

+

+let newline = System.Environment.NewLine // "\r\n"

+

+let rec Indent i =

+  if i = 0 then "" else " " + (Indent (i-1))

+

+let rec PrintSep sep f list =

+  match list with

+  | [] -> ""

+  | [a] -> f a

+  | a :: more -> (f a) + sep + (PrintSep sep f more)
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs
index 6f9f9de5..cb9fb06e 100644
--- a/Jennisys/Jennisys/Printer.fs
+++ b/Jennisys/Jennisys/Printer.fs
@@ -2,14 +2,7 @@
 

 open Ast

 open AstUtils

-

-let newline = System.Environment.NewLine // "\r\n"

-

-let rec PrintSep sep f list =

-  match list with

-  | [] -> ""

-  | [a] -> f a

-  | a :: more -> (f a) + sep + (PrintSep sep f more)

+open PrintUtils     

   

 let rec PrintType ty =

   match ty with

@@ -25,17 +18,18 @@ let PrintVarDecl vd =
   | Var(id,None) -> id

   | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty)

 

-let PrintVarName vd =

-  match vd with

-  | Var(id,_) -> id

-

 let rec PrintExpr ctx expr =

   match expr with

   | IntLiteral(d)     -> sprintf "%d" d

   | BoolLiteral(b)    -> sprintf "%b" b

+  | BoxLiteral(id)    -> sprintf "box_%s" id

   | ObjLiteral(id)

   | VarLiteral(id) 

   | IdLiteral(id)     -> id

+  | VarDeclExpr(vlist, declare) -> 

+      let decl = if declare then "var " else ""

+      let vars = PrintSep ", " PrintVarDecl vlist

+      sprintf "%s%s" decl vars

   | Star              -> "*"

   | Dot(e,id)         -> sprintf "%s.%s" (PrintExpr 100 e) id

   | UnaryExpr(op,UnaryExpr(op2, e2))   -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))

@@ -56,13 +50,14 @@ let rec PrintExpr ctx expr =
       let openParen = if needParens then "(" else ""

       let closeParen = if needParens then ")" else ""

       sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen

-  | MethodCall(rcv,name,aparams) ->

+  | MethodCall(rcv,_,name,aparams) ->

       sprintf "%s.%s(%s)" (PrintExpr 0 rcv) name (aparams |> PrintSep ", " (PrintExpr 0))

 

 let rec PrintConst cst = 

   match cst with 

   | IntConst(v)        -> sprintf "%d" v

   | BoolConst(b)       -> sprintf "%b" b

+  | BoxConst(id)       -> sprintf "box_%s" id

   | VarConst(v)        -> sprintf "%s" v

   | SetConst(cset)     -> sprintf "{%s}" (PrintSep " " (fun c -> PrintConst c) (Set.toList cset))

   | SeqConst(cseq)     -> sprintf "[%s]" (PrintSep " " (fun c -> PrintConst c) cseq)

@@ -80,19 +75,18 @@ let PrintSig signature =
         else ""

       sprintf "(%s)%s" (ins |> PrintSep ", " PrintVarDecl) returnClause

 

-let rec Indent i =

-  if i = 0 then "" else " " + (Indent (i-1))

-

-let rec PrintStmt stmt indent =

+let rec PrintStmt stmt indent printNewline =

   let idt = (Indent indent)

+  let nl = if printNewline then newline else ""

   match stmt with

   | Block(stmts) ->

-      idt + "{" + newline +

-      (PrintStmtList stmts (indent + 2)) +

-      idt + "}" + newline

-  | Assign(lhs,rhs) -> sprintf "%s%s := %s%s" idt (PrintExpr 0 lhs) (PrintExpr 0 rhs) newline

-and PrintStmtList stmts indent =

-  stmts |> List.fold (fun acc s -> acc + (PrintStmt s indent)) ""

+      idt + "{" + nl +

+      (PrintStmtList stmts (indent + 2) true) +

+      idt + "}" + nl

+  | Assign(lhs,rhs) -> sprintf "%s%s := %s%s" idt (PrintExpr 0 lhs) (PrintExpr 0 rhs) nl

+  | ExprStmt(expr) -> sprintf "%s%s%s" idt (PrintExpr 0 expr) nl

+and PrintStmtList stmts indent printNewline =

+  stmts |> List.fold (fun acc s -> acc + (PrintStmt s indent printNewline)) ""

 

 let PrintRoutine signature pre body =

   let preStr = pre |> ForeachConjunct (fun e -> sprintf "    requires %s%s" (PrintExpr 0 e) newline)

diff --git a/Jennisys/Jennisys/Resolver.fs b/Jennisys/Jennisys/Resolver.fs
index 46d14746..b86b782f 100644
--- a/Jennisys/Jennisys/Resolver.fs
+++ b/Jennisys/Jennisys/Resolver.fs
@@ -15,12 +15,20 @@ open DafnyModelUtils
 

 type Obj = { name: string; objType: Type }

 

+type AssignmentType = 

+  | FieldAssignment of (Obj * VarDecl) * Expr // the first string is the symbolic name of an object literal

+  | ArbitraryStatement of Stmt

+

 type HeapInstance = {

-   assignments: ((Obj * VarDecl) * Expr) list; // the first string is the symbolic name of an object literal

+   objs: Map<string, Obj>;

+   assignments: AssignmentType list

    methodArgs: Map<string, Const>;

+   methodRetVals: Map<string, Expr>;

    globals: Map<string, Expr>;

 }

 

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

+

 // resolving values

 exception ConstResolveFailed of string

  

@@ -76,7 +84,11 @@ let TryResolve hModel cst =
 /// If unable to resolve, raises a ConstResolveFailed exception

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

 let Resolve hModel cst =

-  ResolveCont hModel (fun c _ -> raise (ConstResolveFailed("failed to resolve " + c.ToString()))) cst

+  ResolveCont hModel (fun c _ -> 

+                        match c with

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

+                        | _ -> failwithf "internal error: expected Unresolved but got %O" c

+                     ) cst //fun c _ -> raise (ConstResolveFailed("failed to resolve " + c.ToString()))

  

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

 /// Evaluates a given expression with respect to a given heap instance       

@@ -94,8 +106,12 @@ let Eval heapInst resolveExprFunc expr =
           | ObjLiteral("this") | ObjLiteral("null") -> expr

           | IdLiteral("this")  | IdLiteral("null") -> failwith "should never happen anymore" //TODO

           | VarLiteral(id) -> 

-              let argValue = heapInst.methodArgs |> Map.tryFind id |> Utils.ExtractOptionMsg ("cannot find value for method parameter " + id)

-              argValue |> Const2Expr

+              match heapInst.methodArgs |> Map.tryFind id with

+              | Some(argValue) -> argValue |> Const2Expr

+              | None -> 

+                  match heapInst.methodRetVals |> Map.tryFind id with

+                  | Some(e) -> e

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

           | IdLiteral(id) ->

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

               match globalVal with

@@ -105,9 +121,9 @@ let Eval heapInst resolveExprFunc expr =
       | Some(fldName) -> 

           match expr with

           | ObjLiteral(objName) -> 

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

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

               match h2 with

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

+              | FieldAssignment((_,_),x) :: [] -> 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)

@@ -120,37 +136,58 @@ let Eval heapInst resolveExprFunc expr =
 /// (HeapInstance), where all fields for all objects have explicit 

 /// assignments.

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

-let ResolveModel hModel = 

+let ResolveModel hModel outArgs = 

   let hmap = hModel.heap |> Map.fold (fun acc (o,f) l ->

-                                        let objName, objType = match Resolve hModel o with

-                                                               | ThisConst(_,t) -> "this", t;

-                                                               | NewObj(name, t) -> PrintGenSym name, t

-                                                               | _ -> failwith ("unresolved object ref: " + o.ToString())

-                                        let objType = objType |> Utils.ExtractOptionMsg "unknown object type"

+                                        let objName, objTypeOpt = match Resolve hModel o with

+                                                                  | ThisConst(_,t) -> "this", t;

+                                                                  | NewObj(name, t) -> PrintGenSym name, t

+                                                                  | _ -> failwith ("unresolved object ref: " + o.ToString())

+                                        let objType = objTypeOpt |> Utils.ExtractOptionMsg "unknown object type"

+                                        let obj = {name = objName; objType = objType}

                                         let value = TryResolve hModel l |> Const2Expr

-                                        Utils.ListMapAdd ({name = objName; objType = objType}, f) value acc 

+                                        Utils.ListMapAdd (obj, f) value acc 

                                      ) []

-  let argmap = hModel.env |> Map.fold (fun acc k v -> 

-                                         match k with

-                                         | VarConst(name) -> acc |> Map.add name (Resolve hModel v)

-                                         | _ -> acc

-                                      ) Map.empty 

-  { assignments = hmap; 

-    methodArgs  = argmap; 

-    globals     = Map.empty }

+                         |> List.map (fun el -> FieldAssignment(el))

+  let objs = hmap |> List.fold (fun acc asgn -> 

+                                  match asgn with

+                                  | FieldAssignment((obj,_),_) -> acc |> Map.add obj.name obj

+                                  | _ -> acc) Map.empty

+  let argmap, retvals = hModel.env |> Map.fold (fun (acc1,acc2) k v -> 

+                                                  match k with

+                                                  | VarConst(name) -> 

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

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

+                                                      else

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

+                                                  | _ -> acc1, acc2

+                                               ) (Map.empty, Map.empty)

+  { objs          = objs;

+    assignments   = hmap; 

+    methodArgs    = argmap; 

+    methodRetVals = retvals;

+    globals       = Map.empty }

 

 let rec GetCallGraph solutions graph = 

+  let rec __SearchExprsForMethodCalls elist acc = 

+    match elist with

+    | e :: rest ->

+        match e with 

+        // no need to descend for, just check if the top-level one is MEthodCall

+        | MethodCall(_,cname,mname,_) -> __SearchExprsForMethodCalls rest (acc |> Set.add (cname,mname))

+        | _ -> __SearchExprsForMethodCalls rest acc 

+    | [] -> acc

   match solutions with

   | ((comp,m), sol) :: rest -> 

         let callees = sol |> List.fold (fun acc (cond, hInst) ->

-                                          let mcalls = hInst.assignments |> List.choose (fun ((obj,_),e) ->

-                                                                                          match e with 

-                                                                                          | MethodCall(_,mname,_) -> 

-                                                                                              let targetCompName = GetTypeShortName obj.objType

-                                                                                              Some(targetCompName, mname)

-                                                                                          | _ -> None)

-                                          acc |> Set.union (mcalls |> Set.ofList)

-                                      ) Set.empty

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

+                                                                            match asgn with

+                                                                            | FieldAssignment(_,e) ->

+                                                                                __SearchExprsForMethodCalls [e] acc

+                                                                            | ArbitraryStatement(stmt) -> 

+                                                                                let exprs = ExtractTopLevelExpressions stmt

+                                                                                __SearchExprsForMethodCalls exprs acc

+                                                                         ) acc

+                                       ) Set.empty

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

         GetCallGraph rest graph'

   | [] -> graph
\ No newline at end of file
diff --git a/Jennisys/Jennisys/SymGen.fs b/Jennisys/Jennisys/SymGen.fs
new file mode 100644
index 00000000..a2e783ad
--- /dev/null
+++ b/Jennisys/Jennisys/SymGen.fs
@@ -0,0 +1,9 @@
+module SymGen

+

+let cnt = ref 0

+

+let NewSym = 

+  let sym = sprintf "x_%d" !cnt

+  cnt := !cnt + 1

+  sym

+   
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Utils.fs b/Jennisys/Jennisys/Utils.fs
index d5251a08..156d427c 100644
--- a/Jennisys/Jennisys/Utils.fs
+++ b/Jennisys/Jennisys/Utils.fs
@@ -158,8 +158,7 @@ let ListMapTryFind key lst =
 let rec ListMapAdd key value lst = 

   match lst with

   | (k,v) :: rest -> if k = key then (k, value) :: rest else (k,v) :: (ListMapAdd key value rest)

-  | [] -> [(key,value)]

-  

+  | [] -> [(key,value)]                                           

 

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

 /// ensures: ret = elem in lst

diff --git a/Jennisys/Jennisys/examples/List.jen b/Jennisys/Jennisys/examples/List.jen
index 63535a20..a7ba26ed 100644
--- a/Jennisys/Jennisys/examples/List.jen
+++ b/Jennisys/Jennisys/examples/List.jen
@@ -33,6 +33,10 @@ class Node[T] {
 
   constructor Double(p: T, q: T)
     ensures list = [p q]
+
+  method List() returns (lst: seq[T])
+    requires |list| = 1
+    ensures lst = list
 }
 
 model Node[T] {
diff --git a/Jennisys/Jennisys/examples/NumberMethods.jen b/Jennisys/Jennisys/examples/NumberMethods.jen
new file mode 100644
index 00000000..91fbc4f9
--- /dev/null
+++ b/Jennisys/Jennisys/examples/NumberMethods.jen
@@ -0,0 +1,40 @@
+class NumberMethods {
+ 
+  method Double(p: int) returns (ret: int)
+    ensures ret = 2*p
+
+  method Sum(a: int, b: int) returns (ret: int)
+    ensures ret = a + b
+
+  method Min2(a: int, b: int) returns (ret: int)
+    ensures a < b ==> ret = a
+    ensures a >= b ==> ret = b
+
+  method Min22(a: int, b: int) returns (ret: int)
+    ensures ret in {a b}
+    ensures ret <= a && ret <= b
+
+  method Min3(a: int, b: int, c: int) returns (ret: int)
+    ensures ret in {a b c}
+    ensures ret <= a && ret <= b && ret <= c
+
+  method Min32(a: int, b: int, c: int) returns (ret: int)
+    ensures ret in {a b c}
+    ensures forall x :: x in {a b c} ==> ret <= x
+
+ method MinSum(a: int, b: int, c: int) returns (ret: int)
+    ensures ret in {a+b a+c b+c}
+    ensures ret <= a+b && ret <= b+c && ret <= a+c
+
+ method Min4(a: int, b: int, c: int, d: int) returns (ret: int)
+    ensures ret in {a b c d}
+    ensures forall x :: x in {a b c d} ==> ret <= x
+
+  method Abs(a: int) returns (ret: int)
+    ensures ret in {a (-a)} && ret >= 0
+
+}
+
+model NumberMethods {
+
+}
\ No newline at end of file
diff --git a/Jennisys/Jennisys/examples/Set.jen b/Jennisys/Jennisys/examples/Set.jen
index b867a007..0bd42701 100644
--- a/Jennisys/Jennisys/examples/Set.jen
+++ b/Jennisys/Jennisys/examples/Set.jen
@@ -14,9 +14,6 @@ class Set {
     requires p != q
     ensures elems = {p q}
 
-  constructor Triple(p: int, q: int, r: int)
-    requires p != q && q != r && r != p
-    ensures elems = {p q r}
 }
 
 model Set {
@@ -36,9 +33,9 @@ class SetNode {
   constructor Init(x: int)
     ensures elems = {x}
 
-  constructor Double(x: int, y: int)
-    requires x != y
-    ensures elems = {x y}
+  constructor Double(a: int, b: int)
+    requires a != b
+    ensures elems = {a b}
 
   constructor DoubleBase(x: int, y: int)
     requires x > y
diff --git a/Jennisys/Jennisys/examples/mod2/jennisys-synth_List.dfy b/Jennisys/Jennisys/examples/mod2/jennisys-synth_List.dfy
index e3f7a701..a87d9b50 100644
--- a/Jennisys/Jennisys/examples/mod2/jennisys-synth_List.dfy
+++ b/Jennisys/Jennisys/examples/mod2/jennisys-synth_List.dfy
@@ -33,6 +33,9 @@ class List<T> {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p, q];

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

   {

     var gensym68 := new Node<T>;

     gensym68.Double(p, q);

@@ -48,6 +51,7 @@ class List<T> {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [];

+    ensures |list| == 0;

   {

     this.list := [];

     this.root := null;

@@ -61,6 +65,8 @@ class List<T> {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [t];

+    ensures list[0] == t;

+    ensures |list| == 1;

   {

     var gensym67 := new Node<T>;

     gensym67.Init(t);

@@ -110,6 +116,9 @@ class Node<T> {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p, q];

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

   {

     var gensym74 := new Node<T>;

     gensym74.Init(q);

@@ -126,6 +135,8 @@ class Node<T> {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [t];

+    ensures list[0] == t;

+    ensures |list| == 1;

   {

     this.data := t;

     this.list := [t];

diff --git a/Jennisys/Jennisys/examples/mod2/jennisys-synth_List2.dfy b/Jennisys/Jennisys/examples/mod2/jennisys-synth_List2.dfy
index 08268640..27c2d3b3 100644
--- a/Jennisys/Jennisys/examples/mod2/jennisys-synth_List2.dfy
+++ b/Jennisys/Jennisys/examples/mod2/jennisys-synth_List2.dfy
@@ -33,6 +33,9 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p] + [q];

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

   {

     var gensym67 := new IntNode;

     gensym67.Double(p, q);

@@ -48,6 +51,7 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [];

+    ensures |list| == 0;

   {

     this.list := [];

     this.root := null;

@@ -61,13 +65,11 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [1, 2];

+    ensures list[0] == 1;

+    ensures list[1] == 2;

+    ensures |list| == 2;

   {

-    var gensym65 := new IntNode;

-    gensym65.Double(1, 2);

-    this.list := [1, 2];

-    this.root := gensym65;

-    // repr stuff

-    this.Repr := {this} + this.root.Repr;

+    this.Double(1, 2);

   }

 

 

@@ -76,6 +78,8 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p];

+    ensures list[0] == p;

+    ensures |list| == 1;

   {

     var gensym66 := new IntNode;

     gensym66.Init(p);

@@ -91,13 +95,10 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [2];

+    ensures list[0] == 2;

+    ensures |list| == 1;

   {

-    var gensym65 := new IntNode;

-    gensym65.Init(2);

-    this.list := [2];

-    this.root := gensym65;

-    // repr stuff

-    this.Repr := {this} + this.root.Repr;

+    this.Singleton(2);

   }

 

 

@@ -106,13 +107,10 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p + q];

+    ensures list[0] == p + q;

+    ensures |list| == 1;

   {

-    var gensym67 := new IntNode;

-    gensym67.Init(p + q);

-    this.list := [p + q];

-    this.root := gensym67;

-    // repr stuff

-    this.Repr := {this} + this.root.Repr;

+    this.Singleton(p + q);

   }

 

 

@@ -121,13 +119,11 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p] + [p + 1];

+    ensures list[0] == p;

+    ensures list[1] == p + 1;

+    ensures |list| == 2;

   {

-    var gensym66 := new IntNode;

-    gensym66.Double(p, p + 1);

-    this.list := [p] + [p + 1];

-    this.root := gensym66;

-    // repr stuff

-    this.Repr := {this} + this.root.Repr;

+    this.Double(p, p + 1);

   }

 

 }

@@ -165,25 +161,14 @@ class IntNode {
   }

 

 

-  method SingletonZero()

-    modifies this;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures list == [0];

-  {

-    this.data := 0;

-    this.list := [0];

-    this.next := null;

-    // repr stuff

-    this.Repr := {this};

-  }

-

-

   method Double(x: int, y: int)

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [x, y];

+    ensures list[0] == x;

+    ensures list[1] == y;

+    ensures |list| == 2;

   {

     var gensym74 := new IntNode;

     gensym74.Init(y);

@@ -200,6 +185,8 @@ class IntNode {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [x];

+    ensures list[0] == x;

+    ensures |list| == 1;

   {

     this.data := x;

     this.list := [x];

@@ -208,6 +195,18 @@ class IntNode {
     this.Repr := {this};

   }

 

+

+  method SingletonZero()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [0];

+    ensures list[0] == 0;

+    ensures |list| == 1;

+  {

+    this.Init(0);

+  }

+

 }

 

 

diff --git a/Jennisys/Jennisys/examples/mod2/jennisys-synth_List3.dfy b/Jennisys/Jennisys/examples/mod2/jennisys-synth_List3.dfy
index 9eba9fe6..56fa4b7b 100644
--- a/Jennisys/Jennisys/examples/mod2/jennisys-synth_List3.dfy
+++ b/Jennisys/Jennisys/examples/mod2/jennisys-synth_List3.dfy
@@ -33,6 +33,9 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p] + [q];

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

   {

     var gensym68 := new IntNode;

     gensym68._synth_IntList_Double_gensym68(p, q);

@@ -48,6 +51,7 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [];

+    ensures |list| == 0;

   {

     this.list := [];

     this.root := null;

@@ -61,13 +65,11 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [1, 2];

+    ensures list[0] == 1;

+    ensures list[1] == 2;

+    ensures |list| == 2;

   {

-    var gensym65 := new IntNode;

-    gensym65._synth_IntList_OneTwo_gensym65();

-    this.list := [1, 2];

-    this.root := gensym65;

-    // repr stuff

-    this.Repr := {this} + this.root.Repr;

+    this.Double(1, 2);

   }

 

 

@@ -76,6 +78,8 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p];

+    ensures list[0] == p;

+    ensures |list| == 1;

   {

     var gensym67 := new IntNode;

     gensym67._synth_IntList_Singleton_gensym67(p);

@@ -91,13 +95,10 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [2];

+    ensures list[0] == 2;

+    ensures |list| == 1;

   {

-    var gensym66 := new IntNode;

-    gensym66._synth_IntList_SingletonTwo_gensym66();

-    this.list := [2];

-    this.root := gensym66;

-    // repr stuff

-    this.Repr := {this} + this.root.Repr;

+    this.Singleton(2);

   }

 

 

@@ -106,13 +107,10 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p + q];

+    ensures list[0] == p + q;

+    ensures |list| == 1;

   {

-    var gensym68 := new IntNode;

-    gensym68._synth_IntList_Sum_gensym68(p, q);

-    this.list := [p + q];

-    this.root := gensym68;

-    // repr stuff

-    this.Repr := {this} + this.root.Repr;

+    this.Singleton(p + q);

   }

 

 

@@ -121,13 +119,11 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p] + [p + 1];

+    ensures list[0] == p;

+    ensures list[1] == p + 1;

+    ensures |list| == 2;

   {

-    var gensym67 := new IntNode;

-    gensym67._synth_IntList_TwoConsecutive_gensym67(p);

-    this.list := [p] + [p + 1];

-    this.root := gensym67;

-    // repr stuff

-    this.Repr := {this} + this.root.Repr;

+    this.Double(p, p + 1);

   }

 

 }

@@ -185,11 +181,26 @@ class IntNode {
     ensures Valid();

     ensures data == p + 1;

   {

-    this.data := p + 1;

-    this.next := null;

-    this.succ := [];

+    this.Init(p + 1);

+  }

+

+

+  method OneTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == 1;

+    ensures |succ| == 1;

+    ensures succ[0] != null;

+    ensures succ[0].data == 2;

+  {

+    var gensym73 := new IntNode;

+    gensym73._synth_IntNode_OneTwo_gensym73();

+    this.data := 1;

+    this.next := gensym73;

+    this.succ := [gensym73];

     // repr stuff

-    this.Repr := {this};

+    this.Repr := {this} + this.next.Repr;

   }

 

 

@@ -199,6 +210,7 @@ class IntNode {
     ensures Valid();

     ensures data == 0;

     ensures succ == [];

+    ensures |succ| == 0;

   {

     this.data := 0;

     this.next := null;

@@ -216,6 +228,7 @@ class IntNode {
     ensures |succ| == 1;

     ensures succ[0].data == q;

     ensures succ[0].succ == [];

+    ensures |succ[0].succ| == 0;

   {

     var gensym80 := new IntNode;

     gensym80._synth_IntNode__synth_IntList_Double_gensym68_gensym80(q);

@@ -227,40 +240,6 @@ class IntNode {
   }

 

 

-  method _synth_IntList_OneTwo_gensym65()

-    modifies this;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures data == 1;

-    ensures |succ| == 1;

-    ensures succ[0].data == 2;

-    ensures succ[0].succ == [];

-  {

-    var gensym78 := new IntNode;

-    gensym78._synth_IntNode__synth_IntList_OneTwo_gensym65_gensym78();

-    this.data := 1;

-    this.next := gensym78;

-    this.succ := [gensym78];

-    // repr stuff

-    this.Repr := {this} + this.next.Repr;

-  }

-

-

-  method _synth_IntList_SingletonTwo_gensym66()

-    modifies this;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures data == 2;

-    ensures |succ| == 0;

-  {

-    this.data := 2;

-    this.next := null;

-    this.succ := [];

-    // repr stuff

-    this.Repr := {this};

-  }

-

-

   method _synth_IntList_Singleton_gensym67(p: int)

     modifies this;

     ensures fresh(Repr - {this});

@@ -276,59 +255,6 @@ class IntNode {
   }

 

 

-  method _synth_IntList_Sum_gensym68(p: int, q: int)

-    modifies this;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures data == p + q;

-    ensures |succ| == 0;

-  {

-    this.data := p + q;

-    this.next := null;

-    this.succ := [];

-    // repr stuff

-    this.Repr := {this};

-  }

-

-

-  method _synth_IntList_TwoConsecutive_gensym67(p: int)

-    modifies this;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures data == p;

-    ensures |succ| == 1;

-    ensures succ[0].data == p + 1;

-    ensures succ[0].succ == [];

-  {

-    var gensym79 := new IntNode;

-    gensym79._synth_IntNode__synth_IntList_TwoConsecutive_gensym67_gensym79(p);

-    this.data := p;

-    this.next := gensym79;

-    this.succ := [gensym79];

-    // repr stuff

-    this.Repr := {this} + this.next.Repr;

-  }

-

-

-  method OneTwo()

-    modifies this;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures data == 1;

-    ensures |succ| == 1;

-    ensures succ[0] != null;

-    ensures succ[0].data == 2;

-  {

-    var gensym73 := new IntNode;

-    gensym73._synth_IntNode_OneTwo_gensym73();

-    this.data := 1;

-    this.next := gensym73;

-    this.succ := [gensym73];

-    // repr stuff

-    this.Repr := {this} + this.next.Repr;

-  }

-

-

   method _synth_IntNode_OneTwo_gensym73()

     modifies this;

     ensures fresh(Repr - {this});

@@ -358,36 +284,6 @@ class IntNode {
     this.Repr := {this};

   }

 

-

-  method _synth_IntNode__synth_IntList_OneTwo_gensym65_gensym78()

-    modifies this;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures data == 2;

-    ensures |succ| == 0;

-  {

-    this.data := 2;

-    this.next := null;

-    this.succ := [];

-    // repr stuff

-    this.Repr := {this};

-  }

-

-

-  method _synth_IntNode__synth_IntList_TwoConsecutive_gensym67_gensym79(p: int)

-    modifies this;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures data == p + 1;

-    ensures |succ| == 0;

-  {

-    this.data := p + 1;

-    this.next := null;

-    this.succ := [];

-    // repr stuff

-    this.Repr := {this};

-  }

-

 }

 

 

diff --git a/Jennisys/Jennisys/examples/mod2/jennisys-synth_Number.dfy b/Jennisys/Jennisys/examples/mod2/jennisys-synth_Number.dfy
index 454a8548..0b5504d2 100644
--- a/Jennisys/Jennisys/examples/mod2/jennisys-synth_Number.dfy
+++ b/Jennisys/Jennisys/examples/mod2/jennisys-synth_Number.dfy
@@ -162,7 +162,7 @@ class Number {
     ensures num <= b + c;

     ensures num <= a + c;

   {

-    this.Min3(a + b, a + c, b + c);

+    this.Min3(a + b, b + c, a + c);

   }

 

 

diff --git a/Jennisys/Jennisys/examples/mod2/jennisys-synth_NumberMethods.dfy b/Jennisys/Jennisys/examples/mod2/jennisys-synth_NumberMethods.dfy
new file mode 100644
index 00000000..7e6c68e4
--- /dev/null
+++ b/Jennisys/Jennisys/examples/mod2/jennisys-synth_NumberMethods.dfy
@@ -0,0 +1,176 @@
+class NumberMethods {

+  ghost var Repr: set<object>;

+

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    true

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    true

+  }

+

+

+  method Abs(a: int) returns (ret: int)

+    modifies this;

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a, -a};

+    ensures ret >= 0;

+  {

+    if (-a >= 0) {

+      ret := -a;

+    } else {

+      ret := a;

+    }

+  }

+

+

+  method Double(p: int) returns (ret: int)

+    modifies this;

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == 2 * p;

+  {

+    ret := 2 * p;

+  }

+

+

+  method Min2(a: int, b: int) returns (ret: int)

+    modifies this;

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures a < b ==> ret == a;

+    ensures a >= b ==> ret == b;

+  {

+    if (a >= b ==> a == b) {

+      ret := a;

+    } else {

+      ret := b;

+    }

+  }

+

+

+  method Min22(a: int, b: int) returns (ret: int)

+    modifies this;

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a, b};

+    ensures ret <= a;

+    ensures ret <= b;

+  {

+    if (a <= b) {

+      ret := a;

+    } else {

+      ret := b;

+    }

+  }

+

+

+  method Min3(a: int, b: int, c: int) returns (ret: int)

+    modifies this;

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a, b, c};

+    ensures ret <= a;

+    ensures ret <= b;

+    ensures ret <= c;

+  {

+    ret := this.Min32(a, b, c);

+  }

+

+

+  method Min32(a: int, b: int, c: int) returns (ret: int)

+    modifies this;

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a, b, c};

+    ensures ret <= a;

+    ensures ret <= b;

+    ensures ret <= c;

+  {

+    if (a <= b && a <= c) {

+      ret := a;

+    } else {

+      if (c <= a && c <= b) {

+        ret := c;

+      } else {

+        ret := b;

+      }

+    }

+  }

+

+

+  method Min4(a: int, b: int, c: int, d: int) returns (ret: int)

+    modifies this;

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a, b, c, d};

+    ensures ret <= a;

+    ensures ret <= b;

+    ensures ret <= c;

+    ensures ret <= d;

+  {

+    if (a <= b && (a <= c && a <= d)) {

+      ret := a;

+    } else {

+      if (d <= a && (d <= b && d <= c)) {

+        ret := d;

+      } else {

+        if (c <= a && (c <= b && c <= d)) {

+          ret := c;

+        } else {

+          ret := b;

+        }

+      }

+    }

+  }

+

+

+  method MinSum(a: int, b: int, c: int) returns (ret: int)

+    modifies this;

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a + b, a + c, b + c};

+    ensures ret <= a + b;

+    ensures ret <= b + c;

+    ensures ret <= a + c;

+  {

+    ret := this.Min3(a + b, b + c, a + c);

+  }

+

+

+  method Sum(a: int, b: int) returns (ret: int)

+    modifies this;

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == a + b;

+  {

+    ret := a + b;

+  }

+

+}

+

+

diff --git a/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy b/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy
index 8449b03c..a3407cc8 100644
--- a/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy
+++ b/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy
@@ -122,6 +122,54 @@ class SetNode {
   }

 

 

+  method Double(a: int, b: int)

+    modifies this;

+    requires a != b;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {a, b};

+  {

+    if (b > a) {

+      this.DoubleBase(b, a);

+    } else {

+      this.DoubleBase(a, b);

+    }

+  }

+

+

+  method DoubleBase(x: int, y: int)

+    modifies this;

+    requires x > y;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x, y};

+  {

+    var gensym77 := new SetNode;

+    gensym77.Init(x);

+    this.data := y;

+    this.elems := {x, y};

+    this.left := null;

+    this.right := gensym77;

+    // repr stuff

+    this.Repr := {this} + this.right.Repr;

+  }

+

+

+  method Init(x: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x};

+  {

+    this.data := x;

+    this.elems := {x};

+    this.left := null;

+    this.right := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

   method Triple(x: int, y: int, z: int)

     modifies this;

     requires x != y;

@@ -184,54 +232,6 @@ class SetNode {
     this.Repr := ({this} + this.left.Repr) + this.right.Repr;

   }

 

-

-  method Double(x: int, y: int)

-    modifies this;

-    requires x != y;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures elems == {x, y};

-  {

-    if (y > x) {

-      this.DoubleBase(y, x);

-    } else {

-      this.DoubleBase(x, y);

-    }

-  }

-

-

-  method DoubleBase(x: int, y: int)

-    modifies this;

-    requires x > y;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures elems == {x, y};

-  {

-    var gensym77 := new SetNode;

-    gensym77.Init(x);

-    this.data := y;

-    this.elems := {x, y};

-    this.left := null;

-    this.right := gensym77;

-    // repr stuff

-    this.Repr := {this} + this.right.Repr;

-  }

-

-

-  method Init(x: int)

-    modifies this;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures elems == {x};

-  {

-    this.data := x;

-    this.elems := {x};

-    this.left := null;

-    this.right := null;

-    // repr stuff

-    this.Repr := {this};

-  }

-

 }

 

 

diff --git a/Jennisys/Jennisys/tmp.out b/Jennisys/Jennisys/tmp.out
new file mode 100644
index 00000000..9a51a8c8
--- /dev/null
+++ b/Jennisys/Jennisys/tmp.out
@@ -0,0 +1,435 @@
+// 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/Test/dafny1/ListContents.dfy b/Test/dafny1/ListContents.dfy
index f672950b..069ffbde 100644
--- a/Test/dafny1/ListContents.dfy
+++ b/Test/dafny1/ListContents.dfy
@@ -48,7 +48,7 @@ class Node<T> {
     r.footprint := {r} + this.footprint;

     r.list := [r.data] + this.list;

   }

-

+  

   method ReverseInPlace() returns (reverse: Node<T>)

     requires Valid();

     modifies footprint;

diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log
index 2b733bac..ac776509 100644
--- a/_admin/Boogie/aste/summary.log
+++ b/_admin/Boogie/aste/summary.log
@@ -1,9 +1,9 @@
-# Aste started: 2011-06-30 07:00:12

+# Aste started: 2011-08-11 07:00:38

 # Host id: Boogiebox

-# [2011-06-30 07:03:09] SpecSharp revision: 8b896b8f359f

-# [2011-06-30 07:03:09] SscBoogie revision: 8b896b8f359f

-# [2011-06-30 07:04:26] Boogie revision: 16582b67c707

-[2011-06-30 07:07:12] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

+# [2011-08-11 07:04:37] SpecSharp revision: dc85b77ee5c9

+# [2011-08-11 07:04:37] SscBoogie revision: dc85b77ee5c9

+# [2011-08-11 07:06:10] Boogie revision: 3b524cec7850

+[2011-08-11 07:09:01] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

 

     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


@@ -15,8 +15,9 @@
     D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(111,7): warning CS0162: Unreachable code detected


     D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(290,7): warning CS0162: Unreachable code detected


     D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(309,7): warning CS0162: Unreachable code detected


-    D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1665,11): warning CS0162: Unreachable code detected


-    D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1825,11): warning CS0162: Unreachable code detected


+    D:\Temp\aste\Boogie\Source\VCGeneration\StratifiedVC.cs(88,36): warning CS0108: 'VC.StratifiedVCGen.StratifiedInliningInfo.privateVars' hides inherited member 'VC.VCGen.LazyInliningInfo.privateVars'. Use the new keyword if hiding was intended.


+    D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1823,11): warning CS0162: Unreachable code detected


+    D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1983,11): warning CS0162: Unreachable code detected


     D:\Temp\aste\Boogie\Source\VCGeneration\StratifiedVC.cs(668,17): warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.


     warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


@@ -28,8 +29,9 @@
     warning CS0162: Unreachable code detected


     warning CS0162: Unreachable code detected


     warning CS0162: Unreachable code detected


+    warning CS0108: 'VC.StratifiedVCGen.StratifiedInliningInfo.privateVars' hides inherited member 'VC.VCGen.LazyInliningInfo.privateVars'. Use the new keyword if hiding was intended.


     warning CS0162: Unreachable code detected


     warning CS0162: Unreachable code detected


     warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.


-[2011-06-30 07:50:02] 0 out of 30 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

-# [2011-06-30 07:51:05] Released nightly of Boogie

+[2011-08-11 07:51:56] 0 out of 30 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

+# [2011-08-11 07:52:57] Released nightly of Boogie