diff --git a/examples/resource.rs b/examples/resource.rs
index ad91efb4575102bc5a708641919cc4db997fb0e5..24c6f1503f521e44a172f8b3fd44e21c74ba7125 100644
--- a/examples/resource.rs
+++ b/examples/resource.rs
@@ -115,8 +115,8 @@ fn stub_EXTI3() {
 fn idle() -> ! {
     readbasepri();
     stub_EXTI1();
-    stub_EXTI1();
-    stub_EXTI1();
+    stub_EXTI2();
+    stub_EXTI3();
 
     loop {
         rtfm::nop();
diff --git a/klee_stm_gdb.py b/klee_stm_gdb.py
index 03c5318350ae4de87ef2810c75c7b9f963d3413a..2e3c86975348cdc3dcd4c11018abec1a638b5290 100644
--- a/klee_stm_gdb.py
+++ b/klee_stm_gdb.py
@@ -141,8 +141,10 @@ class MainBP(gdb.Breakpoint):
             print("Tasks: ", tasks)
             print("Name of task to test:", tasks[task_to_test])
             if not task_to_test == -1:
-                gdb.write('Task to call: %s \n' % tasks[task_to_test])
-                gdb.execute('call %s' % tasks[task_to_test])
+                gdb.write('Task to call: %s \n' % "stub_" +
+                          tasks[task_to_test])
+                gdb.execute('call %s' % "stub_" +
+                            tasks[task_to_test] + "()")
             else:
                 print("No task defined")
                 """