diff --git a/examples/sht/shard.ivy b/examples/sht/shard.ivy
index 7910250..2112738 100644
--- a/examples/sht/shard.ivy
+++ b/examples/sht/shard.ivy
@@ -19,17 +19,12 @@ module table_shard(key,data) = {
 	second(Y:range) : data
     }
 
+    instance iter : order_iterator(range)
+
     function value(S:t,X:key):data
 
-    instance iter : order_iterator(range)
-    
     derived at(S,X,Y) = (first(S,Y) = X & second(S,Y) ~= 0)
-    derived find(S,X) = some Y. at(S,X,Y)
-    derived present(S,X) = at(S,X,find(S,X))
-	
-    definition value(S,X) = second(S,find(S,X)) if present(S,X) else 0
-
-    conjecture at(S,X,Y) & at(S,X,Z) -> Y = Z
+    definition value(S:t,x:key) = some Y. at(S,x,Y) in second(S,Y) else 0
 
     object impl = {
 	
diff --git a/examples/sht/table.ivy b/examples/sht/table.ivy
index a59bb85..a103e37 100644
--- a/examples/sht/table.ivy
+++ b/examples/sht/table.ivy
@@ -36,8 +36,8 @@ module hash_table(key,value,shard) = {
 
 	after extract_ {
 	    assert shard.lo(res) = lo;
-	    assert shard.hi(res) = hi;
-	    assert (lo <= X & X <= hi) -> shard.value(res,X) = hash(X)
+	    assert shard.hi(res) <= hi;
+	    assert (shard.lo(res) <= X & X <= shard.hi(res)) -> shard.value(res,X) = hash(X)
 	}
 
 	before incorporate(s:shard.t) {
@@ -69,6 +69,10 @@ module hash_table(key,value,shard) = {
 		while ~shard.iter.iter_end(pos) & idx <= lim
 		    invariant ~shard.iter.done(X,pos) -> shard.second(res,X) = 0
                     invariant lo <= X & key.iter.done(X,idx) -> shard.value(res,X) = hash(X)  
+		    invariant ~key.iter.iter_end(idx) -> lo <= key.iter.iter_val(idx)
+		    invariant shard.iter.iter_end(pos) -> key.iter.done(lo,idx)
+		    invariant ~key.iter.done(X,idx) -> ~shard.at(res,X,Y)
+		    invariant shard.at(res,X,Y) & shard.at(res,X,Z) -> Y = Z
 		{
 		    shard.first(res,shard.iter.val(pos)) := key.iter.val(idx);
 		    shard.second(res,shard.iter.val(pos)) := tab.get(key.iter.val(idx));
@@ -76,10 +80,10 @@ module hash_table(key,value,shard) = {
 		    pos := shard.iter.next(pos)
 		};		
 		shard.lo(res) := lo;
-		if key.iter.begin(hi) <= idx {
+		if key.iter.done(hi,idx) {
 		    shard.hi(res) := hi
 		} else {
-		    shard.hi(res) := key.iter.val(idx)
+		    shard.hi(res) := key.iter.val(key.iter.prev(idx))
 		}
 	    }
 	}
@@ -109,6 +113,7 @@ module hash_table(key,value,shard) = {
 
 	conjecture tab.s(X) & tab.r(X,Y) -> hash(X) = Y
 	conjecture ~tab.s(X) -> hash(X) = 0
+	conjecture tab.s(X) -> tab.r(X,hash(X))
     }
 
 }
diff --git a/ivy/include/collections.ivy b/ivy/include/collections.ivy
index cc90009..e7d0f7b 100644
--- a/ivy/include/collections.ivy
+++ b/ivy/include/collections.ivy
@@ -284,7 +284,7 @@ module ordered_map(key,value) = {
 	}
 
 	after get {
-	    assert r(k,v) & s(k) | v = 0
+	    assert r(k,v) & s(k) | ~s(k) & v = 0
 	}
 
 	# erase elements in a closed interval
diff --git a/ivy/include/order.ivy b/ivy/include/order.ivy
index 9bcf56f..ccf879c 100644
--- a/ivy/include/order.ivy
+++ b/ivy/include/order.ivy
@@ -20,6 +20,7 @@ module order_iterator(range) = {
     action begin(x:range) returns (y:t)
     action end returns (y:t)
     action next(x:t) returns (y:t)
+    action prev(y:t) returns (x:t)
     action val(x:t) returns (y:range)
     action over(x:t) returns (y:bool)
     
@@ -40,6 +41,17 @@ module order_iterator(range) = {
 	           | ~(iter_val(x) < Y & Y < iter_val(y))
 	             & iter_val(x) < iter_val(y) & ~iter_end(y)
 	}
+
+	before prev {
+	    assert iter_end(y) | exists X. X < iter_val(y)
+	}
+	after prev {
+	    assert ~iter_end(x);
+	    assert X <= iter_val(x) & iter_end(y)
+	           | ~(iter_val(x) < Y & Y < iter_val(y))
+	             & iter_val(x) < iter_val(y) & ~iter_end(y)
+	}
+
 	before val {
 	    assert ~iter_end(x)
 	}
diff --git a/ivy/ivy_actions.py b/ivy/ivy_actions.py
index f498720..8027772 100644
--- a/ivy/ivy_actions.py
+++ b/ivy/ivy_actions.py
@@ -16,6 +16,13 @@ from ivy_ast import AST, compose_atoms, MixinAfterDef
 import ivy_module
 import ivy_utils as iu
 
+def p_c_a(s):
+    a = s.split(':')
+    return (a[0]+'.ivy',int(a[1]))
+
+checked_assert = iu.Parameter("assert","",check=lambda s: len(s.split(':'))==2,
+                              process=p_c_a)
+
 class Schema(AST):
     def __init__(self,defn,fresh):
         self.defn,self.fresh = defn,fresh
@@ -232,6 +239,11 @@ class AssertAction(Action):
     def action_update(self,domain,pvars):
         type_check(domain,self.args[0])
 #        print type(self.args[0])
+        ca = checked_assert.get()
+        if ca:
+            if ca != self.lineno:
+                return ([],formula_to_clauses(self.args[0]),false_clauses())
+        iu.dbg('self')
         cl = formula_to_clauses(dual_formula(self.args[0]))
 #        return ([],formula_to_clauses_tseitin(self.args[0]),cl)
         return ([],true_clauses(),cl)
@@ -677,22 +689,20 @@ class WhileAction(Action):
     def __str__(self):
         res = 'while ' + str(self.args[0]) + '\n'
         for inv in self.args[2:]:
-            res += 'invariant ' + str(inv) + '\n'
+            res += 'invariant ' + str(inv.args[0]) + '\n'
         res += bracket_action(self.args[1])
         return res
     def expand(self,domain,pvars):
         modset,pre,post = self.args[1].int_update(domain,pvars)  # TODO:cheaper way to get modset
-        asserts = [AssertAction(fmla) for fmla in self.args[2:]]
-        assumes = [AssumeAction(fmla) for fmla in self.args[2:]]
+        asserts = self.args[2:]
+        assumes = [a.assert_to_assume() for a in asserts]
         havocs = [HavocAction(sym) for sym in modset]
-        for a in asserts + assumes:
-            a.lineno = self.lineno #TODO: get actual invariant lineno
         res =  Sequence(*(
                 asserts +
                 havocs +
                 assumes +
                 [ChoiceAction(Sequence(),Sequence(*([AssumeAction(self.args[0]),
-                                                     self.args[1]]+asserts))),
+                                                     self.args[1]]+asserts+[AssumeAction(And())]))),
                 AssumeAction(Not(self.args[0]))]))
         return res
             
diff --git a/ivy/ivy_check.py b/ivy/ivy_check.py
index cb9f656..4821e8c 100644
--- a/ivy/ivy_check.py
+++ b/ivy/ivy_check.py
@@ -58,6 +58,18 @@ def usage():
     print "usage: \n  {} file.ivy".format(sys.argv[0])
     sys.exit(1)
 
+def find_assertions():
+    res = []
+    for actname,action in im.module.actions.iteritems():
+        for a in action.iter_subactions():
+            if isinstance(a,act.AssertAction):
+                res.append(a)
+    return res
+
+def show_assertions():
+    for a in find_assertions():
+        print '{}: {}'.format(a.lineno,a)
+
 def check_module():
     # If user specifies an isolate, check it. Else, if any isolates
     # are specificied in the file, check all, else check globally.
@@ -86,6 +98,7 @@ def check_module():
         with im.module.copy():
             ivy_isolate.create_isolate(isolate) # ,ext='ext'
             with im.module.theory_context():
+                print im.module.sig.symbols
                 check_properties()
                 ag = ivy_art.AnalysisGraph(initializer=ivy_alpha.alpha)
                 if im.module.initializers:
@@ -94,12 +107,19 @@ def check_module():
                         display_cex("safety failed in initializer",cex)
                 with ivy_interp.EvalContext(check=False):
                     check_conjectures('Initiation','These conjectures are false initially.',ag,ag.states[0])
+                    show_assertions()
+                    assertions = find_assertions()
                     for a in sorted(im.module.public_actions):
                         print "trying {}...".format(a)
-                        ag.execute_action(a,prestate=ag.states[0])
-                        cex = ag.check_bounded_safety(ag.states[-1])
-                        if cex is not None:
-                            display_cex("safety failed",cex)
+                        tried = set()
+                        for asn in assertions:
+                            if asn.lineno not in tried:
+                                tried.add(asn.lineno)
+                                act.checked_assert.value = asn.lineno
+                                ag.execute_action(a,prestate=ag.states[0])
+                                cex = ag.check_bounded_safety(ag.states[-1])
+                                if cex is not None:
+                                    display_cex("safety failed",cex)
                         check_conjectures('Consecution','These conjectures are not inductive.',ag,ag.states[-1])
 
 
diff --git a/ivy/ivy_compiler.py b/ivy/ivy_compiler.py
index 52484db..3ceb154 100644
--- a/ivy/ivy_compiler.py
+++ b/ivy/ivy_compiler.py
@@ -357,23 +357,29 @@ def compile_action_def(a,sig):
         return res
 
 def compile_defn(df):
-    if isinstance(df.args[1],ivy_ast.SomeExpr):
-        ifval = df.args[1].if_value() or df.args[1].params()[0]
-        elseval = df.args[1].else_value() or ifval
-        eqn = ivy_ast.Forall(df.args[1].params(),
-                             ivy_ast.Atom('=',(df.args[0],ivy_ast.Ite(df.args[1].fmla(),ifval,elseval))))
-        fmla = sortify_with_inference(eqn)
-        args = [list(fmla.variables)[0],fmla.body.args[1].args[0]]
-        if df.args[1].if_value() :
-            args.append(fmla.body.args[1].args[1])
-        if df.args[1].else_value() :
-            args.append(fmla.body.args[1].args[2])
-        df = ivy_logic.Definition(fmla.body.args[0],ivy_logic.Some(*args))
-    else:
-        eqn = ivy_ast.Atom('=',(df.args[0],df.args[1]))
-        eqn = sortify_with_inference(eqn)
-        df = ivy_logic.Definition(eqn.args[0],eqn.args[1])
-    return df
+    has_consts = any(not isinstance(p,ivy_ast.Variable) for p in df.args[0].args)
+    sig = ivy_logic.sig.copy() if has_consts else ivy_logic.sig
+    with sig:
+        for p in df.args[0].args:
+            if not isinstance(p,ivy_ast.Variable):
+                compile_const(p,sig)
+        if isinstance(df.args[1],ivy_ast.SomeExpr):
+            ifval = df.args[1].if_value() or df.args[1].params()[0]
+            elseval = df.args[1].else_value() or ifval
+            eqn = ivy_ast.Forall(df.args[1].params(),
+                                 ivy_ast.Atom('=',(df.args[0],ivy_ast.Ite(df.args[1].fmla(),ifval,elseval))))
+            fmla = sortify_with_inference(eqn)
+            args = [list(fmla.variables)[0],fmla.body.args[1].args[0]]
+            if df.args[1].if_value() :
+                args.append(fmla.body.args[1].args[1])
+            if df.args[1].else_value() :
+                args.append(fmla.body.args[1].args[2])
+            df = ivy_logic.Definition(fmla.body.args[0],ivy_logic.Some(*args))
+        else:
+            eqn = ivy_ast.Atom('=',(df.args[0],df.args[1]))
+            eqn = sortify_with_inference(eqn)
+            df = ivy_logic.Definition(eqn.args[0],eqn.args[1])
+        return df
     
     
 class IvyDomainSetup(IvyDeclInterp):
diff --git a/ivy/ivy_logic.py b/ivy/ivy_logic.py
index b3fd832..ccef1cc 100644
--- a/ivy/ivy_logic.py
+++ b/ivy/ivy_logic.py
@@ -494,6 +494,22 @@ def is_epr_rec(term,uvars):
 def is_epr(term):
     return is_epr_rec(term,lu.free_variables(term))
 
+def variables(sorts):
+    return [Variable('V'+str(idx),s) for idx,s in enumerate(sorts)]
+
+def extensionality(destrs):
+    if not destrs:
+        return Or()
+    c = []
+    sort = destrs[0].sort.dom[0]
+    x,y = Variable("X",sort),Variable("Y",sort)
+    for d in destrs:
+        vs = variables(d.sort.dom[1:])
+        c.append(Equals(d(*([x]+vs)),d(*([y]+vs))))
+    res = Implies(And(*c),Equals(x,y))
+    iu.dbg('res')
+    return res
+    
 Variable = lg.Var
 Variable.args = property(lambda self: [])
 Variable.clone = lambda self,args: self
@@ -942,6 +958,8 @@ def close_formula(fmla):
     else:
         return ForAll(variables,fmla)
 
+free_variables = lu.free_variables
+
 def uninterpreted_sorts():
     return [s for s in sig.sorts.values() if isinstance(s,UninterpretedSort) and s.name not in sig.interp]
 
diff --git a/ivy/ivy_logic_utils.py b/ivy/ivy_logic_utils.py
index 6bae19e..9d33100 100644
--- a/ivy/ivy_logic_utils.py
+++ b/ivy/ivy_logic_utils.py
@@ -1119,9 +1119,9 @@ def dual_formula(fmla, skolemizer=None):
     fmla = negate(substitute_ast(fmla,sksubs))
     if instantiator != None: 
         gts = ground_apps_ast(fmla)
-        insts = instantiate(ground_terms)
+        insts = clauses_to_formula(instantiator(gts))
         fmla = And(fmla,insts)
-    return negate(fmla)
+    return fmla
 
 def reskolemize_clauses(clauses, skolemizer):
     print clauses
diff --git a/ivy/ivy_module.py b/ivy/ivy_module.py
index 6c1d298..69f913e 100644
--- a/ivy/ivy_module.py
+++ b/ivy/ivy_module.py
@@ -84,18 +84,9 @@ class Module(object):
         return res
 
     def background_theory(self, symbols=None):
-        """ Return a set of clauses which represent the background theory
-        restricted to the given symbols (should be like the result of used_symbols).
-        """
-        theory = list(self.get_axioms())
-        # axioms of the derived relations TODO: used only the
-        # referenced ones, but we need to know abstract domain for
-        # this
-        for ldf in self.definitions:
-            cnst = ldf.formula.to_constraint()
-            if il.is_epr(cnst):
-                theory.append(cnst) # TODO: make this a def?
-        return lu.Clauses(theory)
+        if hasattr(self,"theory"):
+            return self.theory
+        return lu.Clauses([])
 
     def add_to_hierarchy(self,name):
         if iu.ivy_compose_character in name:
@@ -123,10 +114,28 @@ class Module(object):
 
     def theory_context(self):
         """ Set up to instiate the non-epr axioms """
+        """ Return a set of clauses which represent the background theory
+        restricted to the given symbols (should be like the result of used_symbols).
+        """
+        theory = list(self.get_axioms())
+        # axioms of the derived relations TODO: used only the
+        # referenced ones, but we need to know abstract domain for
+        # this
+        for ldf in self.definitions:
+            cnst = ldf.formula.to_constraint()
+            if all(isinstance(p,il.Variable) for p in ldf.formula.args[0].args):
+                theory.append(cnst) # TODO: make this a def?
+        # extensionality axioms for structs
+        for sort in sorted(self.sort_destructors):
+            destrs = self.sort_destructors[sort]
+            if any(d.name in self.sig.symbols for d in destrs):
+                theory.append(il.extensionality(destrs))
+        self.theory = lu.Clauses(theory)
+
         non_epr = {}
         for ldf in self.definitions:
             cnst = ldf.formula.to_constraint()
-            if not il.is_epr(cnst):
+            if not all(isinstance(p,il.Variable) for p in ldf.formula.args[0].args):
                 non_epr[ldf.formula.defines()] = (ldf,cnst)
         return ModuleTheoryContext(functools.partial(instantiate_non_epr,non_epr))
         
@@ -152,10 +161,11 @@ def instantiate_non_epr(non_epr,ground_terms):
         for term in ground_terms:
             if term.rep in non_epr and term not in matched:
                 ldf,cnst = non_epr[term.rep]
-                subst = dict((v.name,t) for v,t in zip(ldf.formula.args[0].args,term.args))
-                inst = lu.substitute_ast(cnst,subst)
-                if il.is_epr(inst):
-                    theory.append(inst)
+                subst = dict((v,t) for v,t in zip(ldf.formula.args[0].args,term.args)
+                             if not isinstance(v,il.Variable))
+                inst = lu.substitute_constants_ast(cnst,subst)
+                theory.append(inst)
+                iu.dbg('inst')
                 matched.add(term)
     return lu.Clauses(theory)
 
diff --git a/ivy/ivy_parser.py b/ivy/ivy_parser.py
index f5df5fc..8f658a7 100644
--- a/ivy/ivy_parser.py
+++ b/ivy/ivy_parser.py
@@ -1004,8 +1004,9 @@ else:
         'invariants : invariants INVARIANT fmla'
         p[0] = p[1]
         inv = p[3]
-        inv.lineno = get_lineno(p,1)
-        p[0].append(inv)
+        a = AssertAction(inv)
+        a.lineno = get_lineno(p,2)
+        p[0].append(a)
 
     def p_action_while_fmla_invariants_lcb_action_rcb(p):
         'action : WHILE fmla invariants LCB action RCB'
@@ -1166,10 +1167,33 @@ def p_defns_defns_comma_defn(p):
     p[0] = p[1]
     p[0].append(p[3])
 
-def p_defnlhs_atom(p):
-    'defnlhs : atom'
-    p[0] = p[1]
+def p_defnlhs_symbol(p):
+    'defnlhs : SYMBOL'
+    p[0] = Atom(p[1],[])
+    p[0].lineno = get_lineno(p,1)
     
+def p_defnlhs_symbol_lparen_defargs_rparen(p):
+    'defnlhs : SYMBOL LPAREN defargs RPAREN'
+    p[0] = Atom(p[1],p[3])
+    p[0].lineno = get_lineno(p,1)
+    
+def p_defargs_defarg(p):
+    'defargs : defarg'
+    p[0] = [p[1]]
+
+def p_defargs_defargs_comma_defarg(p):
+    'defargs : defargs COMMA defarg'
+    p[0] = p[1]
+    p[0].append(p[3])
+
+def p_defarg_lparam(p):
+    'defarg : lparam'
+    p[0] = p[1]
+
+def p_defarg_var(p):
+    'defarg : var'
+    p[0] = p[1]
+
 def p_defnlhs_lp_term_relop_term_rp(p):
     'defnlhs : LPAREN term relop term RPAREN'
     p[0] = Atom(p[3],[p[2],p[4]])
diff --git a/ivy/ivy_solver.py b/ivy/ivy_solver.py
index ad6f0a3..32f8b4d 100644
--- a/ivy/ivy_solver.py
+++ b/ivy/ivy_solver.py
@@ -856,7 +856,7 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con
         if res == z3.unsat:
             return None
 
-#    print "shrinking model {"
+    print "shrinking model {"
     for x in chain(sorts_to_minimize, relations_to_minimize):
         for n in itertools.count(1):
             s.push()
@@ -867,7 +867,7 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con
                 break
             else:
                 s.pop()
-#    print "} shrinking model"
+    print "} shrinking model"
     m = get_model(s)
     h = HerbrandModel(s,m,used_symbols_clauses(clauses))
     return h
diff --git a/ivy/ivy_theory.py b/ivy/ivy_theory.py
index 3e12358..43a7558 100644
--- a/ivy/ivy_theory.py
+++ b/ivy/ivy_theory.py
@@ -17,9 +17,11 @@ def get_qa_arcs(fmla,ast,pol,univs):
     is_e = il.is_exists(fmla)
     is_a = il.is_forall(fmla)
     if is_e and pol or is_a and not pol:
+        fvs = set(il.free_variables(fmla))
         for u in univs:
-            for e in il.quantifier_vars(fmla):
-                yield (u.sort,e.sort,ast)
+            if u in fvs:
+                for e in il.quantifier_vars(fmla):
+                    yield (u.sort,e.sort,ast)
     if is_e and not pol or is_a and pol:
         for a in get_qa_arcs(fmla.args[0],ast,pol,univs+list(il.quantifier_vars(fmla))):
             yield a
@@ -84,6 +86,8 @@ def get_assumes_and_asserts():
             if isinstance(sa,ia.IfAction):
                 asserts.append((sa.get_cond(),sa))
 
+    for ldf in im.module.definitions:
+        assumes.append(ldf.formula.to_constraint())
     # TODO: check axioms, inits, conjectures
 
     return assumes,asserts
diff --git a/test/derived3.ivy b/test/derived3.ivy
index c65cb82..ab23b03 100644
--- a/test/derived3.ivy
+++ b/test/derived3.ivy
@@ -1,9 +1,22 @@
 #lang ivy1.6
 
 type t
+type q
+type u
+
+function ident(U:u,X:t):q
+relation r(U:u,X:t,Y:q)
+
+definition ident(U:u,x:t) = some Y. r(U,x,Y) in Y else 0
+
+action a = {
+    assert r(U,X,ident(U,X)) | ident(U,X) = 0
+}
+
+conjecture r(U,X,ident(U,X)) | ident(U,X) = 0
+
+property r(U,X,ident(U,X)) | ident(U,X) = 0
+
 
-function ident(X:t):t
 
-definition ident(X) = some Y. X = Y in Y else 0
 
-property ident(Z) = Z