diff --git a/property.ml b/property.ml
index 44146733cbab7a6b8b94cd9221eda254cdbcb568..f6775875e464cf5b025931b5c1437ea279f159a5 100644
--- a/property.ml
+++ b/property.ml
@@ -77,11 +77,16 @@ let rec repr t =
     | Float f -> Format.sprintf "float %f" f
   in
   match t with
-  | Atomic (var, cop, cst) ->
+  | Atomic_cst (var, cop, cst) ->
     let var_s = string_of_var var in
     let cop_s = string_of_cop cop in
     let cst_s = string_of_cst cst in
     Format.sprintf "%s %s %s" var_s cop_s cst_s
+  | Atomic_var (var1, cop, var2) ->
+    let var1_s = string_of_var var1 in
+    let cop_s = string_of_cop cop in
+    let var2_s = string_of_var var2 in
+    Format.sprintf "%s %s %s" var1_s cop_s var2_s
   | And (p1, p2) ->
     Format.sprintf "And (%s, %s)" (repr p1) (repr p2)
 
diff --git a/property_parser.mly b/property_parser.mly
index e10923a5c365695aa07c06ab5d403a51ee5139b5..6cf59262921643bc6992a1867ce7a23baf66124b 100644
--- a/property_parser.mly
+++ b/property_parser.mly
@@ -27,7 +27,9 @@ main:
 
 property:
 | var cop cst
-    { Atomic ($1, $2, $3) }
+    { Atomic_cst ($1, $2, $3) }
+| var cop var
+    { Atomic_var ($1, $2, $3) }
 
 var:
 | i = INPUT
diff --git a/property_syntax.mli b/property_syntax.mli
index 4b4472c391a49c7bcd62dbcaa177ffc3d59c0e2b..c81a3ea031ea53e4b1ce502f7f4e51eff320db16 100644
--- a/property_syntax.mli
+++ b/property_syntax.mli
@@ -15,5 +15,6 @@ type cst =
   | Float of float
 
 type t =
-  | Atomic of var * cop * cst
+  | Atomic_cst of var * cop * cst
+  | Atomic_var of var * cop * var
   | And of t * t
diff --git a/solver.ml b/solver.ml
index 985cebcefde28d956350d0aecc795c0191aa7653..8beda3aadfa6f22d7b2943ead7313253c88c894f 100644
--- a/solver.ml
+++ b/solver.ml
@@ -33,8 +33,10 @@ let rec pp_property_marabou property =
     | Float f -> Stdlib.string_of_float f
   in
   match property with
-  | Atomic ((Input v | Output v), cop, cst) ->
+  | Atomic_cst ((Input v | Output v), cop, cst) ->
     Format.sprintf "%s %s %s" v (string_of_cop cop) (string_of_cst cst)
+  | Atomic_var ((Input v1 | Output v1), cop, (Input v2 | Output v2)) ->
+    Format.sprintf "%s %s %s" v1 (string_of_cop cop) v2
   | And (p1, p2) ->
     let s1 = pp_property_marabou p1 in
     let s2 = pp_property_marabou p2 in