Jennisys: started to work on synthesizing some methods. So far, only

  infrastructural things have been implemented, like handling return parameters,
  generating different "fresh" spec for methods than for constructors,
  adding "Valid()" to method preconditions.

25 files changed, 1268 insertions, 492 deletions

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index 42add00c..a98fa057 100644
--- a/Jennisys/Analyzer.fs
+++ b/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/Ast.fs b/Jennisys/Ast.fs
index ab3dc8bb..d0ad5310 100644
--- a/Jennisys/Ast.fs
+++ b/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/AstUtils.fs b/Jennisys/AstUtils.fs
index dc6534e1..8ac62606 100644
--- a/Jennisys/AstUtils.fs
+++ b/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/CodeGen.fs b/Jennisys/CodeGen.fs
index 85e1fd01..9c2dca77 100644
--- a/Jennisys/CodeGen.fs
+++ b/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/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs
index 43536ceb..73b9415a 100644
--- a/Jennisys/DafnyPrinter.fs
+++ b/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.fsproj b/Jennisys/Jennisys.fsproj
index 37b943c6..b9ec91c6 100644
--- a/Jennisys/Jennisys.fsproj
+++ b/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/MethodUnifier.fs b/Jennisys/MethodUnifier.fs
index 0f675e4d..af59799e 100644
--- a/Jennisys/MethodUnifier.fs
+++ b/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/Modularizer.fs b/Jennisys/Modularizer.fs
index 9bb3da72..b196d4cb 100644
--- a/Jennisys/Modularizer.fs
+++ b/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/Parser.fsy b/Jennisys/Parser.fsy
index e854d749..2dd1eb35 100644
--- a/Jennisys/Parser.fsy
+++ b/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/PrintUtils.fs b/Jennisys/PrintUtils.fs
new file mode 100644
index 00000000..138b5e77
--- /dev/null
+++ b/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/Printer.fs b/Jennisys/Printer.fs
index 6f9f9de5..cb9fb06e 100644
--- a/Jennisys/Printer.fs
+++ b/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/Resolver.fs b/Jennisys/Resolver.fs
index 46d14746..b86b782f 100644
--- a/Jennisys/Resolver.fs
+++ b/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/SymGen.fs b/Jennisys/SymGen.fs
new file mode 100644
index 00000000..a2e783ad
--- /dev/null
+++ b/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/Utils.fs b/Jennisys/Utils.fs
index d5251a08..156d427c 100644
--- a/Jennisys/Utils.fs
+++ b/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/examples/List.jen b/Jennisys/examples/List.jen
index 63535a20..a7ba26ed 100644
--- a/Jennisys/examples/List.jen
+++ b/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/examples/NumberMethods.jen b/Jennisys/examples/NumberMethods.jen
new file mode 100644
index 00000000..91fbc4f9
--- /dev/null
+++ b/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/examples/Set.jen b/Jennisys/examples/Set.jen
index b867a007..0bd42701 100644
--- a/Jennisys/examples/Set.jen
+++ b/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/examples/mod2/jennisys-synth_List.dfy b/Jennisys/examples/mod2/jennisys-synth_List.dfy
index e3f7a701..a87d9b50 100644
--- a/Jennisys/examples/mod2/jennisys-synth_List.dfy
+++ b/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/examples/mod2/jennisys-synth_List2.dfy b/Jennisys/examples/mod2/jennisys-synth_List2.dfy
index 08268640..27c2d3b3 100644
--- a/Jennisys/examples/mod2/jennisys-synth_List2.dfy
+++ b/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/examples/mod2/jennisys-synth_List3.dfy b/Jennisys/examples/mod2/jennisys-synth_List3.dfy
index 9eba9fe6..56fa4b7b 100644
--- a/Jennisys/examples/mod2/jennisys-synth_List3.dfy
+++ b/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/examples/mod2/jennisys-synth_Number.dfy b/Jennisys/examples/mod2/jennisys-synth_Number.dfy
index 454a8548..0b5504d2 100644
--- a/Jennisys/examples/mod2/jennisys-synth_Number.dfy
+++ b/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/examples/mod2/jennisys-synth_NumberMethods.dfy b/Jennisys/examples/mod2/jennisys-synth_NumberMethods.dfy
new file mode 100644
index 00000000..7e6c68e4
--- /dev/null
+++ b/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/examples/mod2/jennisys-synth_Set.dfy b/Jennisys/examples/mod2/jennisys-synth_Set.dfy
index 8449b03c..a3407cc8 100644
--- a/Jennisys/examples/mod2/jennisys-synth_Set.dfy
+++ b/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/tmp.out b/Jennisys/tmp.out
new file mode 100644
index 00000000..9a51a8c8
--- /dev/null
+++ b/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;