diff --git a/Makefile.in b/Makefile.in
index 58bbf4720766084669e17f47ecf9ad6c8ef746a1..76c7fd7e62dcdc80faa0bdc09d63e62cbec30ead 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -218,11 +218,11 @@ LIB_TRANSFORM = simplify_formula inlining split_goal \
 		encoding_sort simplify_array filter_trigger \
 		abstraction close_epsilon lift_epsilon \
 		eliminate_epsilon intro_projections_counterexmp \
-		intro_vc_vars_counterexmp prepare_for_counterexmp \
 		instantiate_predicate smoke_detector \
 		prop_curry eliminate_literal \
 		generic_arg_trans_utils case apply subst \
 		introduction ind_itp destruct cut congruence \
+		intro_vc_vars_counterexmp prepare_for_counterexmp \
 		induction induction_pr matching reflection
 
 LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\
diff --git a/bench/ce/if_decision_branch.mlw b/bench/ce/if_decision_branch.mlw
index 0cba3dcb341b3b7eece948324fecb66a4643772b..cdf26ece222e8ebe586cce52f3af2b2e7f6723c3 100644
--- a/bench/ce/if_decision_branch.mlw
+++ b/bench/ce/if_decision_branch.mlw
@@ -5,7 +5,7 @@ module Main
 
   type path_sel_type = { mutable sel_path : bool}
 
-  val path_selector [@model] [@model_trace:TEMP_NAME]: path_sel_type
+  val path_selector [@model_trace:TEMP_NAME]: path_sel_type
 
 end
 
@@ -19,13 +19,15 @@ module Other
     ensures {result = 5}
   =
     (* The counterexample should contain the node_id 5454 here but not 121 *)
-    if (([@node_id=5454] path_selector).sel_path  <- (a = 1); path_selector.sel_path) then
+    if (path_selector.sel_path <- (a = 1); ([@branch_id=5454] path_selector).sel_path) then
       5
     else
+      begin path_selector.sel_path <- true;
       (* The counterexample should contain the node_id 121 but not 5454 *)
-      if (([@node_id=121] path_selector).sel_path <- (a = 5); path_selector.sel_path) then
+      if (path_selector.sel_path <- (a = 5); ([@branch_id=121] path_selector).sel_path) then
         15
       else
         22
+      end
 
 end
diff --git a/bench/ce/oracles/if_decision_branch_CVC4,1.5_SP.oracle b/bench/ce/oracles/if_decision_branch_CVC4,1.5_SP.oracle
index 1562fb6059abb9b5b8d02c17952c6926dc8403cf..e3b249504d6804eae596c3776db65f1e2b524779 100644
--- a/bench/ce/oracles/if_decision_branch_CVC4,1.5_SP.oracle
+++ b/bench/ce/oracles/if_decision_branch_CVC4,1.5_SP.oracle
@@ -10,11 +10,14 @@ Line 19:
 result, [[@introduced]] = {"type" : "Integer" ,
 "val" : "15" }
 Line 22:
-TEMP_NAME, [[@introduced], [@model],
-[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
+TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
+[@branch_id=5454]] = {"type" : "Boolean" ,
 "val" : false }
-Line 26:
-TEMP_NAME, [[@introduced], [@model],
-[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
+Line 25:
+TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
+"val" : true }
+Line 27:
+TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
+[@branch_id=121]] = {"type" : "Boolean" ,
 "val" : true }
 
diff --git a/bench/ce/oracles/if_decision_branch_CVC4,1.5_WP.oracle b/bench/ce/oracles/if_decision_branch_CVC4,1.5_WP.oracle
index 56033de54c9fd1932f99c7ff2be3dafa74e6e84f..3a295b066958f046e7df11189f8ad9796c81ba59 100644
--- a/bench/ce/oracles/if_decision_branch_CVC4,1.5_WP.oracle
+++ b/bench/ce/oracles/if_decision_branch_CVC4,1.5_WP.oracle
@@ -10,11 +10,11 @@ Line 19:
 result, [[@introduced]] = {"type" : "Integer" ,
 "val" : "15" }
 Line 22:
-TEMP_NAME, [[@introduced], [@model],
-[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
+TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
+[@branch_id=5454]] = {"type" : "Boolean" ,
 "val" : false }
-Line 26:
-TEMP_NAME, [[@introduced], [@model],
-[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
+Line 27:
+TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
+[@branch_id=121]] = {"type" : "Boolean" ,
 "val" : true }
 
diff --git a/bench/ce/oracles/if_decision_branch_Z3,4.6.0_SP.oracle b/bench/ce/oracles/if_decision_branch_Z3,4.6.0_SP.oracle
index 08a921d17e1bfa9fb24b1bd4c376da44e45910ee..8d48f6fc38e978ff3be91ead1b8f067cc2595685 100644
--- a/bench/ce/oracles/if_decision_branch_Z3,4.6.0_SP.oracle
+++ b/bench/ce/oracles/if_decision_branch_Z3,4.6.0_SP.oracle
@@ -10,11 +10,14 @@ Line 19:
 result, [[@introduced]] = {"type" : "Integer" ,
 "val" : "22" }
 Line 22:
-TEMP_NAME, [[@introduced], [@model],
-[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
+TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
+[@branch_id=5454]] = {"type" : "Boolean" ,
 "val" : false }
-Line 26:
-TEMP_NAME, [[@introduced], [@model],
-[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
+Line 25:
+TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
+"val" : true }
+Line 27:
+TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
+[@branch_id=121]] = {"type" : "Boolean" ,
 "val" : false }
 
diff --git a/bench/ce/oracles/if_decision_branch_Z3,4.6.0_WP.oracle b/bench/ce/oracles/if_decision_branch_Z3,4.6.0_WP.oracle
index 0ac66720b11c97d8e302855a98fa0ef8dc66a038..edd47ac5e640615c5e220507d1d18f9ae00d2257 100644
--- a/bench/ce/oracles/if_decision_branch_Z3,4.6.0_WP.oracle
+++ b/bench/ce/oracles/if_decision_branch_Z3,4.6.0_WP.oracle
@@ -10,11 +10,11 @@ Line 19:
 result, [[@introduced]] = {"type" : "Integer" ,
 "val" : "22" }
 Line 22:
-TEMP_NAME, [[@introduced], [@model],
-[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
+TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
+[@branch_id=5454]] = {"type" : "Boolean" ,
 "val" : false }
-Line 26:
-TEMP_NAME, [[@introduced], [@model],
-[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
+Line 27:
+TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
+[@branch_id=121]] = {"type" : "Boolean" ,
 "val" : false }
 
diff --git a/src/printer/cntexmp_printer.ml b/src/printer/cntexmp_printer.ml
index be8fbc6007aad847342ba9fca253a302419ea14c..ba7f86cbb2852322f09bfbbd72f0526a6274ffd0 100644
--- a/src/printer/cntexmp_printer.ml
+++ b/src/printer/cntexmp_printer.ml
@@ -98,6 +98,8 @@ let check_exit_vc_term t in_goal info =
 (* This is used to update info_labels of info in the printer. This takes the
    label informations present in the term and add a location to help pretty
    printing the counterexamples.
+   This also takes the information for if_branching "branch_id=" used by API
+   users.
 *)
 let update_info_labels lsname cur_attrs t ls =
   let cur_l =
@@ -118,7 +120,10 @@ let update_info_labels lsname cur_attrs t ls =
           let attr = create_attribute (attr.attr_string ^ ":loc:" ^ f ^ ":" ^ (string_of_int l)) in
           Sattr.add attr acc
         else
-          acc
+          if Strings.has_prefix "branch_id=" attr.attr_string then
+            Sattr.add attr acc
+          else
+            acc
       ) (Sattr.union t.t_attrs ls.ls_name.id_attrs) cur_l
   in
   Mstr.add lsname updated_attr_labels cur_attrs
diff --git a/src/printer/smtv2.ml b/src/printer/smtv2.ml
index 0e13ea7587459845c17a65fc9bfdbb901ec88fb5..40176c5331143fcc99bc0938b9157383305cf2fb 100644
--- a/src/printer/smtv2.ml
+++ b/src/printer/smtv2.ml
@@ -260,7 +260,7 @@ let rec print_term info fmt t =
 
             let str_ls = sprintf "%a" (print_ident info) ls.ls_name in
             let cur_var = info.info_labels in
-            let new_var = update_info_labels  str_ls cur_var t ls in
+            let new_var = update_info_labels str_ls cur_var t ls in
             let () = info.info_labels <- new_var in
             let vc_term_info = info.info_vc_term in
             if vc_term_info.vc_inside then begin
diff --git a/src/transform/prepare_for_counterexmp.ml b/src/transform/prepare_for_counterexmp.ml
index d24e11aac7b2b1d6b3b685e9647030c7cdbfcb82..15ccc9a5ff81fda6cf5b0b0774d8c71004b9b2af 100644
--- a/src/transform/prepare_for_counterexmp.ml
+++ b/src/transform/prepare_for_counterexmp.ml
@@ -33,6 +33,7 @@ let prepare_for_counterexmp2 env task =
     (* Counter-example will be queried, prepare the task *)
     Debug.dprintf debug "Get ce@.";
     let comp_trans = Trans.seq [
+      Introduction.introduce_premises;
       Intro_vc_vars_counterexmp.intro_vc_vars_counterexmp;
       Intro_projections_counterexmp.intro_projections_counterexmp env
     ] in