diff --git a/.vscode/launch.json b/.vscode/launch.json
index 79a152cb..1e6bc9f1 100644
--- a/.vscode/launch.json
+++ b/.vscode/launch.json
@@ -6,11 +6,11 @@
 			"type": "extensionHost",
 			"request": "launch",
 			"args": [
-				"--extensionDevelopmentPath=${workspaceFolder}/debugger-vscode-extension",
+				"--extensionDevelopmentPath=${workspaceFolder}/debug-ui",
 				"${workspaceFolder}/debug-ui/examples"
 			],
 			"outFiles": [
-				"${workspaceFolder}/debugger-vscode-extension/out/**/*.js"
+				"${workspaceFolder}/debug-ui/out/**/*.js"
 			]
 		},
 	]
diff --git a/.vscode/tasks.json b/.vscode/tasks.json
deleted file mode 100644
index bc782229..00000000
--- a/.vscode/tasks.json
+++ /dev/null
@@ -1,84 +0,0 @@
-{
-    "version": "2.0.0",
-    "tasks": [
-        {
-            "script": "build",
-            "label": "snowpack-build",
-            "type": "npm",
-            "options": {
-                "cwd": "${workspaceFolder}/debugger-vscode-extension"
-            }
-        },
-        {
-            "script": "dev",
-            "label": "snowpack-build-dev",
-            "type": "npm",
-            "problemMatcher": {
-                "owner": "typescript",
-                "fileLocation": "absolute",
-                "pattern": {
-                    "regexp": "^(.*):(\\d+):(\\d+):\\s+(warning|error):\\s+(.*)$",
-                    "file": 1,
-                    "line": 2,
-                    "column": 3,
-                    "severity": 4,
-                    "message": 5
-                },
-                "background": {
-                    "activeOnStart": false,
-                    "beginsPattern": "^\\[nodemon\\] starting",
-                    "endsPattern": "^\\[nodemon\\] clean exit"
-                }
-            },
-            "isBackground": true,
-            "options": {
-                "cwd": "${workspaceFolder}/debugger-vscode-extension"
-            }
-        },
-        {
-            "type": "npm",
-            "script": "watch",
-            "problemMatcher": "$tsc-watch",
-            "isBackground": true,
-            "presentation": {
-                "reveal": "never"
-            },
-            "group": {
-            "kind": "build",
-            "isDefault": true
-            },
-            "dependsOn": ["snowpack-build-dev"],
-            "options": {
-                "cwd": "${workspaceFolder}/debugger-vscode-extension"
-            }
-        }
-    ]
-    // "tasks": [
-    //     {
-    //         "type": "npm",
-    //         "script": "compile",
-    //         "isBackground": false,
-    //         "group": {
-    //             "kind": "build",
-    //             "isDefault": false
-    //         },
-    //         "problemMatcher": "$tsc-watch",
-    //         "options": {
-    //             "cwd": "${workspaceFolder}/debugger-vscode-extension"
-    //         }
-    //     },
-    //     {
-    //         "type": "npm",
-    //         "script": "watch",
-    //         "group": "build",
-    //         "isBackground": true,
-    //         "problemMatcher": [
-    //             "$ts-webpack-watch",
-    //             "$tslint-webpack-watch"
-    //         ],
-    //         "options": {
-    //             "cwd": "${workspaceFolder}/debugger-vscode-extension"
-    //         }
-    //     }
-    // ]
-}
\ No newline at end of file
diff --git a/GillianCore/debugging/debugger/base_debugger.ml b/GillianCore/debugging/debugger/base_debugger.ml
index 3657026f..89a094b6 100644
--- a/GillianCore/debugging/debugger/base_debugger.ml
+++ b/GillianCore/debugging/debugger/base_debugger.ml
@@ -314,15 +314,16 @@ struct
 
     let process_files = Process_files.f
 
-    let has_hit_breakpoint dbg =
-      match dbg.frames with
-      | [] -> false
-      | frame :: _ ->
-          if Hashtbl.mem dbg.breakpoints frame.source_path then
-            let breakpoints = Hashtbl.find dbg.breakpoints frame.source_path in
-            (* Currently only one breakpoint per line is supported *)
-            Breakpoints.mem frame.start_line breakpoints
-          else false
+    (* Currently only one breakpoint per line is supported *)
+    let is_breakpoint ~file ~lines proc =
+      match Hashtbl.find_opt proc.breakpoints file with
+      | None -> false
+      | Some breakpoints ->
+          let rec aux = function
+            | [] -> false
+            | line :: ls -> Breakpoints.mem line breakpoints || aux ls
+          in
+          aux lines
 
     let rec call_stack_to_frames call_stack next_proc_body_idx prog =
       match call_stack with
@@ -613,8 +614,9 @@ struct
         exec_data
 
       let with_lifter_effects f proc_state state =
-        let open Effect.Deep in
+        let open Lift in
         let open Lifter in
+        let open Effect.Deep in
         try_with f ()
           {
             effc =
@@ -626,7 +628,11 @@ struct
                         let step_result =
                           handle_step_effect id case path proc_state state
                         in
-                        Effect.Deep.continue k step_result)
+                        continue k step_result)
+                | IsBreakpoint (file, lines) ->
+                    Some
+                      (fun (k : (a, _) continuation) ->
+                        is_breakpoint ~file ~lines proc_state |> continue k)
                 | _ ->
                     let s = Printexc.to_string (Effect.Unhandled eff) in
                     Fmt.failwith "HORROR: effect leak!\n%s" s);
diff --git a/GillianCore/debugging/lifter/gil_lifter.ml b/GillianCore/debugging/lifter/gil_lifter.ml
index 3e3bf8a8..17eec36a 100644
--- a/GillianCore/debugging/lifter/gil_lifter.ml
+++ b/GillianCore/debugging/lifter/gil_lifter.ml
@@ -1,6 +1,7 @@
 module L = Logging
 module DL = Debugger_log
 open Lifter_intf
+open Syntaxes.Option
 include Gil_lifter_intf
 
 type id = L.Report_id.t [@@deriving yojson]
@@ -27,6 +28,7 @@ functor
       submap : id submap;
       branch_path : branch_path;
       parent : (id * branch_case option) option;
+      loc : (string * int) option;
     }
     [@@deriving to_yojson]
 
@@ -73,8 +75,16 @@ functor
         }
         () =
       let display = Fmt.to_to_string Cmd.pp_indexed cmd_report.cmd in
+      let loc =
+        let annot = cmd_report.annot in
+        let+ loc =
+          Annot.get_origin_loc annot
+          |> Option.map Debugger_utils.location_to_display_location
+        in
+        (loc.loc_source, loc.loc_start.pos_line)
+      in
       let data =
-        { id; display; matches; errors; submap; branch_path; parent }
+        { id; display; matches; errors; submap; branch_path; parent; loc }
       in
       let next =
         match next_kind with
@@ -244,24 +254,22 @@ functor
       Option.get case
 
     let find_next state id case =
-      let next =
-        match (get_exn state.map id).next with
-        | None -> failwith "HORROR - tried to step from FinalCmd!"
-        | Some next -> next
-      in
-      match (next, case) with
-      | Single _, Some _ ->
+      let node = get_exn state.map id in
+      match (node.next, case) with
+      | (None | Some (Single _)), Some _ ->
           failwith "HORROR - tried to step case for non-branch cmd"
-      | Single (None, _), None -> Either.Right None
-      | Single (Some next, _), None -> Either.Left (get_exn state.map next)
-      | Branch nexts, None ->
+      | Some (Single (None, _)), None -> Either.Right None
+      | Some (Single (Some next, _)), None ->
+          Either.Left (get_exn state.map next)
+      | Some (Branch nexts), None ->
           let case = select_case nexts in
           Either.Right (Some case)
-      | Branch nexts, Some case -> (
+      | Some (Branch nexts), Some case -> (
           match List.assoc_opt case nexts with
           | None -> failwith "case not found"
           | Some (None, _) -> Either.Right (Some case)
           | Some (Some next, _) -> Either.Left (get_exn state.map next))
+      | None, None -> Either.Left node
 
     let request_next state id case =
       let path = path_of_id id state in
@@ -305,15 +313,23 @@ functor
       in
       (stop_id, Debugger_utils.Step)
 
+    let is_breakpoint node =
+      match node.data.loc with
+      | None -> false
+      | Some (file, line) -> Effect.perform (IsBreakpoint (file, [ line ]))
+
     let continue state id =
       let open Utils.Syntaxes.Option in
-      let rec aux stack ends =
+      let rec aux ?(first = false) stack ends =
         match stack with
         | [] -> List.rev ends
         | (id, case) :: rest -> (
-            match step state id case with
-            | Either.Left nexts -> aux (nexts @ rest) ends
-            | Either.Right end_id -> aux rest (end_id :: ends))
+            let node = get_exn state.map id in
+            if (not first) && is_breakpoint node then aux rest (id :: ends)
+            else
+              match step state id case with
+              | Either.Left nexts -> aux (nexts @ rest) ends
+              | Either.Right end_id -> aux rest (end_id :: ends))
       in
       let end_ =
         let end_, stack =
@@ -327,7 +343,7 @@ functor
               (None, stack)
         in
         let- () = end_ in
-        let ends = aux stack [] in
+        let ends = aux ~first:true stack [] in
         List.hd ends
       in
       (end_, Debugger_utils.Step)
@@ -335,7 +351,17 @@ functor
     let step_out = continue
 
     (* TODO: breakpoints *)
-    let continue_back t _ = (Option.get t.map.root, Debugger_utils.Step)
+    let continue_back t id =
+      let rec aux id = function
+        | None -> (id, Debugger_utils.Step)
+        | Some (id, _) ->
+            let node = get_exn t.map id in
+            if is_breakpoint node then (id, Breakpoint)
+            else aux id node.data.parent
+      in
+      let node = get_exn t.map id in
+      aux id node.data.parent
+    (* (Option.get t.map.root, Debugger_utils.Step) *)
 
     let init_manual proc_name all_procs =
       let map = Exec_map.make () in
diff --git a/GillianCore/debugging/lifter/lifter_intf.ml b/GillianCore/debugging/lifter/lifter_intf.ml
index b6a23643..af1b0488 100644
--- a/GillianCore/debugging/lifter/lifter_intf.ml
+++ b/GillianCore/debugging/lifter/lifter_intf.ml
@@ -24,6 +24,8 @@ module Types = struct
     | Stop of Logging.Report_id.t option
     | ExecNext of (Logging.Report_id.t option * Branch_case.t option)
   [@@deriving yojson]
+
+  type _ Effect.t += IsBreakpoint : (string * int list) -> bool Effect.t
 end
 
 include Types
diff --git a/kanillian/lib/lifter/kani_c_lifter.ml b/kanillian/lib/lifter/kani_c_lifter.ml
index 878a564e..a7f58e85 100644
--- a/kanillian/lib/lifter/kani_c_lifter.ml
+++ b/kanillian/lib/lifter/kani_c_lifter.ml
@@ -60,6 +60,7 @@ struct
     prev : (id * Branch_case.t option) option;
     callers : id list;
     func_return_label : (string * int) option;
+    loc : (string * int) option;
   }
   [@@deriving yojson]
 
@@ -76,6 +77,7 @@ struct
       callers : id list;
       stack_direction : stack_direction option;
       nest_kind : nest_kind option;
+      loc : (string * int) option;
     }
     [@@deriving to_yojson]
 
@@ -111,6 +113,7 @@ struct
       next_kind : (Branch_case.t, branch_data) next_kind;
       callers : id list;
       stack_direction : stack_direction option;
+      loc : (string * int) option;
     }
     [@@deriving yojson]
 
@@ -170,7 +173,7 @@ struct
             : partial_data) =
         partial
       in
-      let** { id; display; callers; stack_direction; nest_kind } =
+      let** { id; display; callers; stack_direction; nest_kind; loc } =
         Result_utils.of_option
           ~none:"Trying to finish partial with no canonical data!"
           canonical_data
@@ -202,6 +205,7 @@ struct
           next_kind;
           callers;
           stack_direction;
+          loc;
         }
 
     let init () = Hashtbl.create 0
@@ -336,6 +340,7 @@ struct
               callers;
               stack_direction;
               nest_kind = None;
+              loc = None;
             };
         Ok ()
 
@@ -366,8 +371,15 @@ struct
               get_stack_info ~partial exec_data
             in
             let Annot.{ nest_kind; _ } = annot in
+            let loc =
+              let+ loc =
+                annot.origin_loc
+                |> Option.map Debugger_utils.location_to_display_location
+              in
+              (loc.loc_source, loc.loc_start.pos_line)
+            in
             partial.canonical_data <-
-              Some { id; display; callers; stack_direction; nest_kind };
+              Some { id; display; callers; stack_direction; nest_kind; loc };
             Ok ()
         | _ -> Ok ()
 
@@ -548,6 +560,7 @@ struct
               prev;
               next_kind;
               callers;
+              loc;
               _;
             } =
         finished_partial
@@ -563,6 +576,7 @@ struct
           prev;
           callers;
           func_return_label;
+          loc;
         }
       in
       let next =
@@ -861,7 +875,18 @@ struct
     | Either.Left next -> next
     | Either.Right (id, case) -> request_next state id case
 
-  let step_all state id case =
+  let is_breakpoint ~start ~current =
+    let b =
+      let+ file, line = current.data.loc in
+      let- () =
+        let* file', line' = start.data.loc in
+        if file = file' && line = line' then Some false else None
+      in
+      Effect.perform (IsBreakpoint (file, [ line ]))
+    in
+    Option.value b ~default:false
+
+  let step_all ~start state id case =
     let cmd = get_exn state.map id in
     let stack_depth = List.length cmd.data.callers in
     let rec aux ends = function
@@ -870,6 +895,11 @@ struct
           let next_id = step state id case in
           let node = get_exn state.map next_id in
           let ends, nexts =
+            let- () =
+              if is_breakpoint ~start ~current:node then
+                Some (node :: ends, rest)
+              else None
+            in
             match node.next with
             | Some (Single _) -> (ends, (next_id, None) :: rest)
             | Some (Branch nexts) ->
@@ -920,7 +950,7 @@ struct
         | NoSubmap | Proc _ -> None
         | Submap m -> Some m
       in
-      let _ = step_all state submap_id None in
+      let _ = step_all ~start:node state submap_id None in
       ()
     in
     let stop_id = step state id None in
@@ -946,10 +976,11 @@ struct
     (id, Debugger_utils.Step)
 
   let continue state id =
+    let start = get_exn state.map id in
     let rec aux ends = function
       | [] -> ends
       | (id, case) :: rest ->
-          let ends' = step_all state id case in
+          let ends' = step_all ~start state id case in
           let ends', nexts =
             ends'
             |> List.partition_map (fun { data; _ } ->
@@ -968,12 +999,11 @@ struct
     | [] -> continue state id
     | caller_id :: _ -> step_over state caller_id
 
-  let is_breakpoint _ = false (* TODO *)
-
   let continue_back state id =
+    let start = get_exn state.map id in
     let rec aux node =
       let { id; callers; _ } = node.data in
-      if is_breakpoint node then (id, Debugger_utils.Breakpoint)
+      if is_breakpoint ~start ~current:node then (id, Debugger_utils.Breakpoint)
       else
         match previous_step id state with
         | None -> (
@@ -982,7 +1012,7 @@ struct
             | caller_id :: _ -> aux (get_exn state.map caller_id))
         | Some (id, _) -> aux (get_exn state.map id)
     in
-    aux (get_exn state.map id)
+    aux start
 
   let init ~proc_name ~all_procs:_ tl_ast prog =
     let gil_state = Gil.get_state () in
diff --git a/wisl/lib/debugging/wislLifter.ml b/wisl/lib/debugging/wislLifter.ml
index e234ba46..f8aeaf7a 100644
--- a/wisl/lib/debugging/wislLifter.ml
+++ b/wisl/lib/debugging/wislLifter.ml
@@ -82,7 +82,7 @@ struct
     matches : matching list;
     errors : string list;
     mutable submap : id submap;
-    (* branch_path : Branch_case.t list; *)
+    loc : string * int;
     prev : (id * Branch_case.t option) option;
     callers : id list;
     func_return_label : (string * int) option;
@@ -98,16 +98,22 @@ struct
   module Partial_cmds = struct
     type prev = id * Branch_case.t option * id list [@@deriving yojson]
 
+    type canonical_cmd_data = {
+      id : id;
+      display : string;
+      stack_info : id list * stack_direction option;
+      is_loop_end : bool;
+      loc : string * int;
+    }
+    [@@deriving to_yojson]
+
     type partial_data = {
       prev : prev option;
       all_ids : (id * (Branch_case.kind option * Branch_case.case)) Ext_list.t;
       unexplored_paths : (id * Gil_branch_case.t option) Stack.t;
       ends : (Branch_case.case * branch_data) Ext_list.t;
-      mutable id : id option;
-      mutable display : string option;
-      mutable stack_info : (id list * stack_direction option) option;
+      mutable canonical_data : canonical_cmd_data option;
       mutable nest_kind : nest_kind option;
-      mutable is_loop_end : bool;
       matches : matching Ext_list.t;
       errors : string Ext_list.t;
     }
@@ -121,11 +127,8 @@ struct
         all_ids = Ext_list.make ();
         unexplored_paths = Stack.create ();
         ends = Ext_list.make ();
-        id = None;
-        display = None;
-        stack_info = None;
+        canonical_data = None;
         nest_kind = None;
-        is_loop_end = false;
         matches = Ext_list.make ();
         errors = Ext_list.make ();
       }
@@ -143,6 +146,7 @@ struct
       submap : id submap;
       callers : id list;
       stack_direction : stack_direction option;
+      loc : string * int;
     }
     [@@deriving yojson]
 
@@ -194,19 +198,7 @@ struct
       is_loop_func && get_fun_call_name exec_data = Some proc_name
 
     let finish ~exec_data partial =
-      let ({
-             prev;
-             all_ids;
-             id;
-             display;
-             stack_info;
-             ends;
-             nest_kind;
-             matches;
-             errors;
-             is_loop_end;
-             _;
-           }
+      let ({ prev; all_ids; ends; nest_kind; matches; errors; _ }
             : partial_data) =
         partial
       in
@@ -214,17 +206,12 @@ struct
         let+ id, branch, _ = prev in
         (id, branch)
       in
-      let** id =
-        id |> Option.to_result ~none:"Trying to finish partial with no id!"
-      in
-      let** display =
-        display
-        |> Option.to_result ~none:"Trying to finish partial with no display!"
-      in
-      let** callers, stack_direction =
-        stack_info
-        |> Option.to_result ~none:"Trying to finish partial with no stack info!"
+      let** { id; display; stack_info; loc; is_loop_end } =
+        partial.canonical_data
+        |> Option.to_result
+             ~none:"Trying to finish partial with no canonical data!"
       in
+      let callers, stack_direction = stack_info in
       let all_ids = all_ids |> Ext_list.to_list |> List.map fst in
       let matches = matches |> Ext_list.to_list in
       let errors = errors |> Ext_list.to_list in
@@ -252,6 +239,7 @@ struct
           display;
           callers;
           stack_direction;
+          loc;
           matches;
           errors;
           submap;
@@ -338,21 +326,24 @@ struct
           ~proc_name
           ~exec_data
           (partial : partial_data) =
-        match (partial.display, annot.stmt_kind, annot.origin_id) with
+        match (partial.canonical_data, annot.stmt_kind, annot.origin_id) with
         | None, (Normal _ | Return _), Some origin_id ->
-            let** display =
+            let** display, is_loop_end =
               match get_origin_node_str tl_ast (Some origin_id) with
-              | Some display -> Ok display
+              | Some display -> Ok (display, false)
               | None ->
                   if is_loop_end ~is_loop_func ~proc_name exec_data then
-                    let () = partial.is_loop_end <- true in
-                    Ok "<end of loop>"
+                    Ok ("<end of loop>", true)
                   else Error "Couldn't get display!"
             in
             let** stack_info = get_stack_info ~partial exec_data in
-            partial.id <- Some id;
-            partial.display <- Some display;
-            partial.stack_info <- Some stack_info;
+            let loc =
+              annot.origin_loc |> Option.get
+              |> Debugger_utils.location_to_display_location
+            in
+            let loc = (loc.loc_source, loc.loc_start.pos_line) in
+            partial.canonical_data <-
+              Some { id; display; stack_info; is_loop_end; loc };
             Ok ()
         | _ -> Ok ()
 
@@ -563,6 +554,7 @@ struct
               prev;
               callers;
               next_kind;
+              loc;
               _;
             } =
         finished_partial
@@ -578,6 +570,7 @@ struct
           prev;
           callers;
           func_return_label;
+          loc;
         }
       in
       let next =
@@ -1011,7 +1004,15 @@ struct
     | Either.Left next -> next
     | Either.Right (id, case) -> request_next state id case
 
-  let step_all state id case =
+  let is_breakpoint ~start ~current =
+    let file, line = current.data.loc in
+    let- () =
+      let file', line' = start.data.loc in
+      if file = file' && line = line' then Some false else None
+    in
+    Effect.perform (IsBreakpoint (file, [ line ]))
+
+  let step_all ~start state id case =
     let cmd = get_exn state.map id in
     let stack_depth = List.length cmd.data.callers in
     let rec aux ends = function
@@ -1020,6 +1021,11 @@ struct
           let next_id = step state id case in
           let node = get_exn state.map next_id in
           let ends, nexts =
+            let- () =
+              if is_breakpoint ~start ~current:node then
+                Some (node :: ends, rest)
+              else None
+            in
             match node.next with
             | Some (Single _) -> (ends, (next_id, None) :: rest)
             | Some (Branch nexts) ->
@@ -1070,7 +1076,7 @@ struct
         | NoSubmap | Proc _ -> None
         | Submap m -> Some m
       in
-      let _ = step_all state submap_id None in
+      let _ = step_all ~start:node state submap_id None in
       ()
     in
     let stop_id = step state id None in
@@ -1096,18 +1102,19 @@ struct
     (id, Debugger_utils.Step)
 
   let continue state id =
+    let start = get_exn state.map id in
     let rec aux ends = function
       | [] -> ends
       | (id, case) :: rest ->
-          let ends' = step_all state id case in
-          let ends', nexts =
-            ends'
+          let new_ends, nexts =
+            let new_ends = step_all ~start state id case in
+            new_ends
             |> List.partition_map (fun { data; _ } ->
                    match get_next_from_end state data with
                    | Some (id, case) -> Either.Right (id, case)
                    | None -> Either.Left data.id)
           in
-          aux (ends @ ends') (nexts @ rest)
+          aux (ends @ new_ends) (nexts @ rest)
     in
     let ends = aux [] [ (id, None) ] in
     let id = List.hd ends in
@@ -1118,12 +1125,11 @@ struct
     | [] -> continue state id
     | caller_id :: _ -> step_over state caller_id
 
-  let is_breakpoint _ = false (* TODO *)
-
   let continue_back state id =
+    let start = get_exn state.map id in
     let rec aux node =
       let { id; callers; _ } = node.data in
-      if is_breakpoint node then (id, Debugger_utils.Breakpoint)
+      if is_breakpoint ~start ~current:node then (id, Debugger_utils.Breakpoint)
       else
         match previous_step id state with
         | None -> (
@@ -1132,7 +1138,7 @@ struct
             | caller_id :: _ -> aux (get_exn state.map caller_id))
         | Some (id, _) -> aux (get_exn state.map id)
     in
-    aux (get_exn state.map id)
+    aux start
 
   let init ~proc_name ~all_procs:_ tl_ast prog =
     let gil_state = Gil.get_state () in