fix for issue #1

ivy/ivy_logic_utils.py

@@ -939,20 +939,27 @@ def elim_definitions(clauses,dead):
     defs = [d for d in clauses.defs if d.defines() not in deadset]
     return Clauses(fmlas,defs)
 
-def elim_dead_definitions(args):
+def rename_symbols(rn,clauses1,to_rename):
+    map1 = dict((s,s.rename(rn)) for s in to_rename)
+    return rename_clauses(clauses1,map1)
+
+
+def elim_dead_definitions(rn,args):
     """ If a symbol defined in one arg occurs free in another,
     then eliminate the definition by converting it to clauses """
     defd = set(d.defines() for a in args for d in a.defs)
     occurs = [set(a.symbols()) for a in args]
-    dead = [sym for sym in defd
-            if not sym.is_skolem() and any (sym not in a.defidx for a in args)]
+    captured = [sym for sym in defd if any (sym not in a.defidx for a in args)]
+    dead = [sym for sym in captured if not sym.is_skolem()]
+    to_rename = [sym for sym in captured if sym.is_skolem()]
+    args = [rename_symbols(rn,arg,to_rename) for arg in args]
 #    print "args = {}, dead = {}".format(args,dead)
     res = [elim_definitions(a,dead) for a in args]
     return res
 
 def or_clauses_int(rn,args):
 #    print "or_clauses_int: args = {}".format(args)
-    args = elim_dead_definitions(args)
+    args = elim_dead_definitions(rn,args)
 #    print "or_clauses_int: args = {}".format(args)
     vs = [bool_const(rn()) for a in args]
     fmlas = ([Or(*vs)]

test/issue1.py

@@ -0,0 +1,58 @@
+
+import ivy.ivy_module as ivy_module
+from ivy.ivy_compiler import ivy_from_string
+from ivy.tk_ui import new_ui
+import ivy.ivy_utils as iu
+
+prog = """#lang ivy1.5
+
+type s
+relation p(X:s)
+individual v:s
+
+relation error
+init ~error
+conjecture ~error
+
+action f returns (u:s) = {
+    assume p(u)
+}
+
+action action1 = {
+    error := true;
+    v := *;
+    assume ~p(v);
+    v := f
+}
+
+action action2 = {
+    v := f;
+    v := *
+}
+
+export action1
+export action2
+"""
+
+with ivy_module.Module():
+    iu.set_parameters({'ui':'cti','ext':'ext'})
+    main_ui = new_ui()
+    ui = main_ui.add(ivy_from_string(prog))
+    main_ui.answer("OK")
+    if ui.check_inductiveness():
+        assert False,"should not have been inductive"
+# #    ui = ui.cti
+#     cg = ui.current_concept_graph
+#     cg.show_relation(cg.relation('link(X,Y)'),'+')
+#     cg.gather()
+#     main_ui.answer("OK")
+#     cg.strengthen()
+#     main_ui.answer("OK")
+#     ui.check_inductiveness()
+# #    cg.show_relation(cg.relation('semaphore'),'+')
+#     cg.gather()
+#     main_ui.answer("View")
+#     cg.bmc_conjecture(bound=1)
+#    main_ui.mainloop()
+
+