diff --git a/klee.py b/klee.py
index 0161b90f23d7a203e6455cda7f6c35a406362a5d..d82351ec031814a293d71c68ba48f86406bfb11d 100644
--- a/klee.py
+++ b/klee.py
@@ -47,12 +47,7 @@ def gdb_set_pc(task):
 def gdb_call(task):
     # call task
     print("#### call task %s" % task)
-    # try:
-    gdb.execute('call %s' % "stub_" + task + "()")
-    #    print("<<<<<<<<<<<<<<<<< after call >>>>>>>>>>>>>>>>>")
-
-    # except gdb.error:
-    #    print("!!!!!!!!!!!!!!!!! after call !!!!!!!!!!!!!!!!!")
+    gdb.execute('call %s' % "stub_" + task + "()"a')
 
 
 def gdb_bkpt_read():
@@ -63,14 +58,14 @@ def gdb_bkpt_read():
 def gdb_setup():
     # Commands for making GDB scriptable
     print("gbd init")
-    # gdb.execute("set confirm off")
-    # gdb.execute("set pagination off")
-    # # gdb.execute("set verbose off")
-    # # gdb.execute("set height 0")
-    # # gdb.execute("set unwindonsignal off")
-    # # gdb.execute("set unwind-on-terminating-exception off")
+    gdb.execute("set confirm off")
+    gdb.execute("set pagination off")
+    gdb.execute("set verbose off")
+    gdb.execute("set height 0")
     # gdb.execute("set unwindonsignal on")
-    gdb.execute("set unwind-on-terminating-exception on")
+    # gdb.execute("set unwindonsignal off")
+    # gdb.execute("set unwind-on-terminating-exception on")
+    # gdb.execute("set unwind-on-terminating-exception off")
 
     gdb.execute("show unwindonsignal")
     gdb.execute("show unwind-on-terminating-exception")
@@ -80,82 +75,73 @@ def gdb_setup():
 
 
 # Event handling
+
+# Ugly hack to avoid race condtitons in the python gdb API
+
+class Executor:
+    def __init__(self, cmd):
+        self.__cmd = cmd
+
+    def __call__(self):
+        gdb.execute(self.__cmd)
+
 # GDB event, called on breakpoint
 
 
 def stop_event(evt):
+    global task_nr
     print("#### stop event %r" % evt)
-    # gdb.execute("finish")
-    # gdb.execute("continue")
-
-    # gdb.execute("break")
     imm = gdb_bkpt_read()
 
     print(" imm = {}".format(imm))
 
     if imm == 0:
         print("-- ordinary breakpoint --")
-        # gdb.execute("return")
-        # gdb_continue()
+        sys.exit(1)
 
     if imm == 1:
-        print("Enter")
-        # gdb.execute("return")
-        # gdb_continue()
+        print(">>>>>>>>>>>>> Enter")
+
+        gdb.post_event(Executor("continue"))
 
     if imm == 2:
-        print("Exit")
-        # gdb.execute("return")
-        # gdb_continue()
+        print("<<<<<<<<<<<<< Exit")
+        gdb.post_event(Executor("continue"))
 
     if imm == 3:
-        print("Finished")
-        next_task()
-        # gdb.execute("return")
-
+        print("------------- Finished")
+        task_nr = task_nr + 1
+        # gdb.execute("si")
+        gdb.execute("return")
 
-def exit_handler(event):
-    print("event type: exit")
-    print("exit code: %d" % (event.exit_code))
+        gdb.post_event(posted_event_init)
 
-# gdb.events.inferior_call_post.connect(exit_handler)
 
-
-def next_task():
+def posted_event_init():
+    print("")
+    print("------------- posted_event_init ")
     global tasks
     global task_nr
-    print("--------------------------- task nr {}".format(task_nr))
+    print("------------- task nr {}".format(task_nr))
 
     if task_nr >= len(tasks):
-        print("--------------------------- tasks done")
+        print("------------- tasks done")
+        gdb.execute("quit")
     else:
         try:
             gdb_call(tasks[task_nr])
-            print("--------------------------- call done, no bkpts")
-            task_nr = task_nr + 1
-            next_task()
-            return
+            print("!!!!!!!!!!!!!!!!!!!!!! ERROR !!!!!!!!!!!!!!!!!!!!!!!!")
+            sys.exit(1)
         except:
-            print("--------------------------- call except, with bkpts wait to be called")
-            task_nr = task_nr + 1
-
+            print("------------- call except")
 
 
 # globals
-tasks = ["EXTI2", "EXTI3", "EXTI3"]
+# tasks = ["EXTI2", "EXTI3", "EXTI3"]
+tasks = ["EXTI3", "EXTI2", "EXTI1"]
 task_nr = 0
 
 print("simple python script started")
 gdb_setup()
 gdb.events.stop.connect(stop_event)
-next_task()
-# gdb.execute("b enter")
-# gdb.execute("b exit")
-
-
-# gdb_set_pc("EXTI1")
-
-# for t_nr, task in enumerate(tasks):
-#     print("-------------- t_nr {}".format(t_nr))
-#     # gdb_set_pc(task)
-#     gdb_call(tasks[t_nr])
+gdb.post_event(posted_event_init)
diff --git a/macros/src/trans.rs b/macros/src/trans.rs
index 01cb0de140989ff8b655852fcf9ec75b1e31c622..1ee0693d05288b47e2644aa0d6816f8a0782f7ed 100644
--- a/macros/src/trans.rs
+++ b/macros/src/trans.rs
@@ -29,7 +29,12 @@ pub fn app(app: &App, ownerships: &Ownerships) -> Tokens {
     quote!(#(#root)*)
 }
 
-fn idle(app: &App, ownerships: &Ownerships, main: &mut Vec<Tokens>, root: &mut Vec<Tokens>) {
+fn idle(
+    app: &App,
+    ownerships: &Ownerships,
+    main: &mut Vec<Tokens>,
+    root: &mut Vec<Tokens>,
+) {
     let krate = krate();
 
     let mut mod_items = vec![];
@@ -547,9 +552,10 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
             for rname in &task.resources {
                 let ceiling = ownerships[rname].ceiling();
                 let _rname = Ident::new(format!("_{}", rname.as_ref()));
-                let resource = app.resources
-                    .get(rname)
-                    .expect(&format!("BUG: resource {} has no definition", rname));
+                let resource = app.resources.get(rname).expect(&format!(
+                    "BUG: resource {} has no definition",
+                    rname
+                ));
 
                 let ty = &resource.ty;
                 let _static = if resource.expr.is_some() {
@@ -707,7 +713,7 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
                 fn #_stub_tname() {
                     #[allow(unsafe_code)]
                     unsafe { #_tname(); }
-                    //unsafe { bkpt_3(); }
+                    unsafe { bkpt_3(); }
                 }
             });
         }