diff --git a/examples/programs/vacid_0_sparse_array.mlw b/examples/programs/vacid_0_sparse_array.mlw
index 9f1fe14e67bff1a032b28bb4ebec61aad4535c4f..1ba985ac696f2059b074ffd60c89f2f0c75f0606 100644
--- a/examples/programs/vacid_0_sparse_array.mlw
+++ b/examples/programs/vacid_0_sparse_array.mlw
@@ -79,9 +79,9 @@ back  +-+-+-+-------------------+
     forall a : sparse_array . invariant a -> 
         let (SA val idx back sz n) = a in
         n = sz -> 
-            permutation sz back and
+            permutation sz back /\
             forall i : int. 0 <= i < sz ->
-                idx#i = dirichlet sz back i and is_elt a i
+                idx#i = dirichlet sz back i /\ is_elt a i
 }
 
 
diff --git a/src/parser/lexer.mll b/src/parser/lexer.mll
index 90e27ae78598889c475c85908e2ecdabcacb15a1..204554847b62f8d3e9487ff60086c9131af01f8a 100644
--- a/src/parser/lexer.mll
+++ b/src/parser/lexer.mll
@@ -189,6 +189,10 @@ rule token = parse
       { ARROW }
   | "<->"
       { LRARROW }
+  | "/\\"
+      { ASYM_AND }
+  | "\\/"
+      { ASYM_OR }
   | "."
       { DOT }
   | "|"
diff --git a/src/parser/parser.mly b/src/parser/parser.mly
index 5bbbdbb097a399d4da66ad28c497fd6a1d83017a..dd5e2edbf119d48b374c38fa1600dcf1a89ff0ee 100644
--- a/src/parser/parser.mly
+++ b/src/parser/parser.mly
@@ -67,7 +67,7 @@
 
 /* symbols */
 
-%token ARROW
+%token ARROW ASYM_AND ASYM_OR
 %token BAR
 %token COLON COMMA
 %token DOT EQUAL
@@ -90,8 +90,8 @@
 
 %nonassoc prec_named
 %right ARROW LRARROW
-%right OR
-%right AND
+%right OR ASYM_OR
+%right AND ASYM_AND
 %nonassoc NOT
 %left EQUAL OP1
 %left OP2
@@ -346,8 +346,12 @@ lexpr:
    { infix_pp $1 PPiff $3 }
 | lexpr OR lexpr
    { infix_pp $1 PPor $3 }
+| lexpr ASYM_OR lexpr
+   { mk_pp (PPnamed ("asym_split", infix_pp $1 PPor $3)) }
 | lexpr AND lexpr
    { infix_pp $1 PPand $3 }
+| lexpr ASYM_AND lexpr
+   { mk_pp (PPnamed ("asym_split", infix_pp $1 PPand $3)) }
 | NOT lexpr
    { prefix_pp PPnot $2 }
 | lexpr EQUAL lexpr
diff --git a/src/programs/pgm_wp.ml b/src/programs/pgm_wp.ml
index 9457b711b44a24c6472a5acb7c0d7c579643e643..034d8de80b479b2ebbd0bf1464f38d2f2e1b5ca9 100644
--- a/src/programs/pgm_wp.ml
+++ b/src/programs/pgm_wp.ml
@@ -39,8 +39,9 @@ let debug = ref false
    TODO: use simp forms / tag with label "WP" *)
 
 let wp_and ?(sym=false) f1 f2 = 
-  (* TODO: tag instead? *)
-  if sym then f_and_simp f1 f2 else f_and_simp f1 (f_implies_simp f1 f2) 
+(*   if sym then f_and_simp f1 f2 else f_and_simp f1 (f_implies_simp f1 f2)  *)
+  let f = f_and_simp f1 f2 in
+  if sym then f else f_label [Split_goal.asym_split] f
 
 let wp_ands ?(sym=false) fl =
   List.fold_left (wp_and ~sym) f_true fl
diff --git a/src/transform/split_goal.ml b/src/transform/split_goal.ml
index 32a87ec34f04de1f75f495b0ce43d0c12570c7d8..69c93cf36639e30dfdb9b2563df595306d1d83c3 100644
--- a/src/transform/split_goal.ml
+++ b/src/transform/split_goal.ml
@@ -33,10 +33,14 @@ let split_case spl c acc tl bl =
   in
   apply_append (f_case tl) acc bll
 
+let asym_split = "asym_split"
+
 let rec split_pos acc f = match f.f_node with
   | Ftrue -> acc
   | Ffalse -> f::acc
   | Fapp _ -> f::acc
+  | Fbinop (Fand,f1,f2) when List.mem asym_split f.f_label ->
+      split_pos (split_pos acc (f_implies f1 f2)) f1
   | Fbinop (Fand,f1,f2) ->
       split_pos (split_pos acc f2) f1
   | Fbinop (Fimplies,f1,f2) ->
@@ -64,10 +68,14 @@ and split_neg acc f = match f.f_node with
   | Fapp _ -> f::acc
   | Fbinop (Fand,f1,f2) ->
       apply_append2 f_and acc (split_neg [] f1) (split_neg [] f2)
+  | Fbinop (Fimplies,f1,f2) when List.mem asym_split f.f_label ->
+      split_neg (split_neg acc (f_and f1 f2)) (f_not f1)
   | Fbinop (Fimplies,f1,f2) ->
       split_neg (split_neg acc f2) (f_not f1)
   | Fbinop (Fiff,f1,f2) ->
       split_neg (split_neg acc (f_and (f_not f1) (f_not f2))) (f_and f2 f1)
+  | Fbinop (For,f1,f2) when List.mem asym_split f.f_label ->
+      split_neg (split_neg acc (f_and (f_not f1) f2)) f1
   | Fbinop (For,f1,f2) ->
       split_neg (split_neg acc f2) f1
   | Fnot f ->
diff --git a/src/transform/split_goal.mli b/src/transform/split_goal.mli
index 752b1e864ff04d03ef4beac332238485cf1a5024..f98e36e36d7de301eca12df25cefcd9226ecb155 100644
--- a/src/transform/split_goal.mli
+++ b/src/transform/split_goal.mli
@@ -17,6 +17,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val asym_split : Term.label
+
 val split_pos : Term.fmla list -> Term.fmla -> Term.fmla list
 val split_neg : Term.fmla list -> Term.fmla -> Term.fmla list
 
diff --git a/tests/test-jcf.why b/tests/test-jcf.why
index 5e8933fc1e5196553b82abe4d993ca15f1fd48cd..94c0b10564dbfe6437be9edaa3140970b5529991 100644
--- a/tests/test-jcf.why
+++ b/tests/test-jcf.why
@@ -1,17 +1,10 @@
 
 (* test file *)
 
-theory Test
-  use export int.Int
-  logic f(int) : int
-  logic q(int, int)
-  axiom A : forall x:int. q (-x) (f x)
-  goal G : 3.14 = 3.15
-end
-
-theory Test2
-  use export list.List
-  goal G : let x = Nil in let t = (Cons 1 x, Cons 3.14 x) in t=t
+theory S
+  use import int.Int
+  logic p int
+  goal G : forall x:int. (p 1 \/ p 2) -> p 3
 end