diff --git a/src/smtinterpol/ir.ml b/src/smtinterpol/ir.ml
index 1416ca83..91b9d3a7 100644
--- a/src/smtinterpol/ir.ml
+++ b/src/smtinterpol/ir.ml
@@ -13,8 +13,10 @@ type rewrite_rule =
   | Rewrite_intern
 
 type split_rule =
-  | Split_xor_1
-  | Split_xor_2
+  | Split_xor_minus_1
+  | Split_xor_minus_2
+  | Split_xor_plus_1
+  | Split_xor_plus_2
   | Split_notOr
 
 type equality_proof =
diff --git a/src/smtinterpol/ir_to_clauses.ml b/src/smtinterpol/ir_to_clauses.ml
index 02c74feb..cee0c994 100644
--- a/src/smtinterpol/ir_to_clauses.ml
+++ b/src/smtinterpol/ir_to_clauses.ml
@@ -354,7 +354,10 @@ let handle_split unsplit_clause split_rule form =
     let first_sub_form = get_subformula heap_form 0 in
     if Form.pform first_sub_form = Form.pform needle_form then 0 else 1 in
   match split_rule with
-  | Split_xor_2 -> 
+  | Split_xor_plus_1 | Split_xor_minus_1 ->
+    let split_clause = lmkOther (ImmBuildDef unsplit_clause) None in
+    split_clause
+  | Split_xor_plus_2 | Split_xor_minus_2 -> 
     let split_clause = lmkOther (ImmBuildDef2 unsplit_clause) None in
     split_clause
   | Split_notOr ->
diff --git a/src/smtinterpol/smtlib_to_ir.ml b/src/smtinterpol/smtlib_to_ir.ml
index 16c10a61..444f6140 100644
--- a/src/smtinterpol/smtlib_to_ir.ml
+++ b/src/smtinterpol/smtlib_to_ir.ml
@@ -56,8 +56,10 @@ let rec walk_equality_proof term =
 *)
 let rec walk_formula_proof term =
   let handle_split_annotation = function
-    | ":xor-1" -> Split_xor_1
-    | ":xor-2" -> Split_xor_2
+    | ":xor-1" -> Split_xor_minus_1
+    | ":xor-2" -> Split_xor_minus_2
+    | ":xor+1" -> Split_xor_plus_1
+    | ":xor+2" -> Split_xor_plus_2
     | ":notOr" -> Split_notOr in
   match (deconstruct_qualidterm term) with
   | "@asserted", [ft] ->