diff --git a/examples/liquid_bsearch2_harder3.ml.target b/examples/liquid_bsearch2_harder3.ml.target
index e564e9c..278b19e 100644
--- a/examples/liquid_bsearch2_harder3.ml.target
+++ b/examples/liquid_bsearch2_harder3.ml.target
@@ -30,9 +30,9 @@ let bsearch
   (fun key vec ->
     let Ex3 xcase =
     let rec look :
-    type (*i*) (*j*) (*k*) b (*0 ≤ k + 1 ∧ 0 ≤ i ∧
-    k + 1 ≤ j*). (b -> (b (* j *)) array -> (* i *) num -> (* k *) num ->
-                     (* k *) ex3)
+    type (*i*) (*k*) (*n*) a (*0 ≤ n + 1 ∧ 0 ≤ k ∧
+    n + 1 ≤ i*). (a -> (a (* i *)) array -> (* k *) num -> (* n *) num ->
+                     (* n *) ex3)
     =
     (fun key vec lo hi ->
       (if lo <= hi then
@@ -44,6 +44,6 @@ let bsearch
         | EQ ->
             (if equal key x then let xcase = m in Ex3 xcase else
             let xcase = -1 in Ex3 xcase))) :
-      (* k *) ex3) else let xcase = -1 in Ex3 xcase)) in
+      (* n *) ex3) else let xcase = -1 in Ex3 xcase)) in
     look key vec 0 (array_length vec + -1) in Ex4 xcase)
 
diff --git a/examples/liquid_gauss_asserted.gadti.target b/examples/liquid_gauss_asserted.gadti.target
index fb69a69..c23387a 100644
--- a/examples/liquid_gauss_asserted.gadti.target
+++ b/examples/liquid_gauss_asserted.gadti.target
@@ -71,4 +71,4 @@ val rowElim :
    ∀i, j, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i ∧ k ≤ j].
    Array (Float, j) → Array (Float, i) → Num k → Num n → ()
 
-val gauss : ∀n[1 ≤ n]. Matrix (n, n + 1) → ()
+val gauss : ∀n[0 ≤ n]. Matrix (n, n + 1) → ()
diff --git a/examples/liquid_gauss_simpler_asserted.gadti.target b/examples/liquid_gauss_simpler_asserted.gadti.target
index e536283..85fd0d9 100644
--- a/examples/liquid_gauss_simpler_asserted.gadti.target
+++ b/examples/liquid_gauss_simpler_asserted.gadti.target
@@ -71,4 +71,4 @@ external rowElim :
    ∀i, j, k, n[0 ≤ n ∧ n + 1 ≤ i ∧ k ≤ i ∧ k ≤ j].
    Array (Float, j) → Array (Float, i) → Num k → Num n → ()
 
-val gauss : ∀n[1 ≤ n]. Matrix (n, n + 1) → ()
+val gauss : ∀n[0 ≤ n]. Matrix (n, n + 1) → ()
diff --git a/examples/liquid_simplex_step_3a.gadti.target b/examples/liquid_simplex_step_3a.gadti.target
index 9e9f098..798c347 100644
--- a/examples/liquid_simplex_step_3a.gadti.target
+++ b/examples/liquid_simplex_step_3a.gadti.target
@@ -44,4 +44,4 @@ external is_neg_aux :
 external is_neg :
    ∀i, k, n[1 ≤ k ∧ n ≤ i + 1]. Matrix (k, i) → Num n → Bool
 
-val main_step3_test : ∀k, n[1 ≤ n ∧ 3 ≤ k]. Matrix (n, k) → Float
+val main_step3_test : ∀k, n[1 ≤ n ∧ 2 ≤ k]. Matrix (n, k) → Float
diff --git a/src/Abduction.ml b/src/Abduction.ml
index 691d98e..6db1333 100644
--- a/src/Abduction.ml
+++ b/src/Abduction.ml
@@ -33,7 +33,7 @@ let residuum q prem concl =
   let concl = to_formula concl in
   solve ~use_quants:false q (subst_formula prem concl)
 
-type t_validation = (VarSet.t * subst) list
+type t_validation = (VarSet.t * (subst * NumS.state)) list
 (* Result remembers the invariant parameters [bvs]. *)
 exception Result of VarSet.t * var_name list * subst * t_validation
 
@@ -243,16 +243,19 @@ let connecteds_vs tvs sb =
 (* FIXME: do we need to check the state of numerical constraints? *)
 let validate q validation added_vs x t lc =
   List.map
-    (fun (br_vs, state as br) ->
+    (fun (br_vs, (state_typ, state_num) as br) ->
        if not (VarSet.is_empty (VarSet.inter added_vs br_vs))
        then
          try
-           let t', _ = VarMap.find x state in
+           let t', _ = VarMap.find x state_typ in
            let upd =
-             unify ~use_quants:false ~sb:state q [Eqty (t, t', lc)] in
-           VarSet.union added_vs br_vs, upd.cnj_typ
+             unify ~use_quants:false ~sb:state_typ q [Eqty (t, t', lc)] in
+           let state_num =
+             NumS.satisfiable_exn ~state:state_num upd.cnj_num in
+           VarSet.union added_vs br_vs, (upd.cnj_typ, state_num)
          with Not_found ->
-           VarSet.union added_vs br_vs, VarMap.add x (t, lc) state
+           VarSet.union added_vs br_vs,
+           (VarMap.add x (t, lc) state_typ, state_num)
        else br)
     validation
 
@@ -748,13 +751,14 @@ module TermAbd = struct
   type discarded = answer
   (* premise including alien premise, conclusion *)
   type branch = sep_formula * subst
-  type br_state = subst
+  type br_state = subst * NumS.state
   type validation = t_validation
 
   let abd_fail_timeout = fail_timeout_count
   let abd_fail_flag = abd_fail_flag
 
-  let abd_simple (obvs, q, dissociate) ~discard ~validation ~neg_validate
+  let abd_simple (obvs, q, dissociate) ~discard ~validation
+      ~validate ~neg_validate
       (bvs, acc) br =
     abd_simple q ~obvs ~bvs ~dissociate ~validation ~neg_validate
         ~discard 0 acc br
@@ -804,8 +808,9 @@ let abd_typ q ~bvs ?(dissociate=false) ~validation ~neg_validate ~discard
     else brs in
   (*[* Format.printf "abd_typ: alien_eqs=%a@\n%!"
     pr_subst !alien_eqs; *]*)
+  let validate _ _ = () in
   let cand_bvs, (vs, ans) =
-    JCA.abd (bvs, q, dissociate) ~discard validation ~neg_validate
+    JCA.abd (bvs, q, dissociate) ~discard validation ~validate ~neg_validate
       (bvs, ([], VarMap.empty)) brs in
   (*[* Format.printf "abd_typ: result vs=%s@\nans=%a@\n%!"
     (String.concat ","(List.map var_str vs))
@@ -843,28 +848,28 @@ let abd_typ q ~bvs ?(dissociate=false) ~validation ~neg_validate ~discard
 let abd_mockup_num q ~bvs brs =
   (* Do not change the order and no. of branches afterwards. *)
   let brs_typ, brs_num = List.split
-    (map_some (fun (prem, concl) ->
-      let prems_opt =
-        try Some (unify ~use_quants:false q prem)
-        with Contradiction _ -> None in
-      match prems_opt with
-      | Some prem ->
-        if List.exists
-          (function CFalse _ -> true | _ -> false) prem.cnj_so
-        then None
-        else                          (* can raise Contradiction *)
-          let {cnj_typ=concl_typ; cnj_num=concl_num; cnj_so=concl_so} =
-            solve ~use_quants:false q concl in
-          List.iter (function
-          | CFalse loc ->
-            raise (Contradiction (Type_sort,
-                                  "assert false is possible", None, loc))
-          | _ -> ()) concl_so;
-          if not (is_right (NumS.satisfiable concl_num)) then None
-          else Some ((prem, concl_typ),
-                     (prem.cnj_num, concl_num))
-      | None -> None)
-       brs) in
+      (map_some (fun (prem, concl) ->
+           let prems_opt =
+             try Some (unify ~use_quants:false q prem)
+             with Contradiction _ -> None in
+           match prems_opt with
+           | Some prem ->
+             if List.exists
+                 (function CFalse _ -> true | _ -> false) prem.cnj_so
+             then None
+             else                          (* can raise Contradiction *)
+               let {cnj_typ=concl_typ; cnj_num=concl_num; cnj_so=concl_so} =
+                 solve ~use_quants:false q concl in
+               List.iter (function
+                   | CFalse loc ->
+                     raise (Contradiction (Type_sort,
+                                           "assert false is possible", None, loc))
+                   | _ -> ()) concl_so;
+               if not (is_right (NumS.satisfiable concl_num)) then None
+               else Some ((prem, concl_typ),
+                          (prem.cnj_num, concl_num))
+           | None -> None)
+          brs) in
   let verif_brs = List.map2
       (fun (prem, concl_ty) (_, concl_num) ->
          VarSet.union (fvs_sb prem.cnj_typ)
@@ -874,17 +879,18 @@ let abd_mockup_num q ~bvs brs =
          prem, concl_ty, concl_num)
       brs_typ brs_num in
   let validation =
-    List.map
-    (fun (br_vs, prem, concl_ty, concl_num) ->
-        (* Do not use quantifiers, because premise is in the conjunction. *)
-        (* TODO: after cleanup optimized in abd_simple, pass clean_ans
-           and remove cleanup here *)
-        let {cnj_typ=sb_ty; cnj_num=_(* ans_num *); cnj_so=_} =
-          combine_sbs q [prem.cnj_typ; concl_ty] in
-        (* let cnj_num = ans_num @ prem.cnj_num @ concl_num in *)
-        (* FIXME: need num state? *)
-        br_vs, (sb_ty (*, NumS.satisfiable cnj_num*)))
-    verif_brs in
+    map_some
+      (fun (br_vs, prem, concl_ty, concl_num) ->
+         (* Do not use quantifiers, because premise is in the conjunction. *)
+         (* TODO: after cleanup optimized in abd_simple, pass clean_ans
+            and remove cleanup here *)
+         try
+           let {cnj_typ=sb_ty; cnj_num=ans_num; cnj_so=_} =
+             combine_sbs q [prem.cnj_typ; concl_ty] in
+           let cnj_num = ans_num @ prem.cnj_num @ concl_num in
+           Some (br_vs, (sb_ty, NumS.satisfiable_exn cnj_num))
+         with Contradiction _ -> None)
+      verif_brs in
   let neg_validate _ = 0 in
   try
     let cand_bvs, alien_eqs, tvs, ans_typ, more_in_brs =
@@ -951,17 +957,19 @@ let abd q ~bvs ~xbvs ?orig_ren ?b_of_v ~upward_of ~nonparam_vars
          prem, concl_ty, concl_num)
       brs_typ brs_num in
   let validation =
-    List.map
-    (fun (br_vs, prem, concl_ty, concl_num) ->
-        (* Do not use quantifiers, because premise is in the conjunction. *)
-        (* TODO: after cleanup optimized in abd_simple, pass clean_ans
-           and remove cleanup here *)
-        let {cnj_typ=sb_ty; cnj_num=_(* ans_num *); cnj_so=_} =
-          combine_sbs q [prem.cnj_typ; concl_ty] in
-        (* let cnj_num = ans_num @ prem.cnj_num @ concl_num in *)
-        (* FIXME: need num state? *)
-        br_vs, (sb_ty (*, NumS.satisfiable cnj_num*)))
-    verif_brs in
+    map_some
+      (fun (br_vs, prem, concl_ty, concl_num) ->
+         try
+           (* Do not use quantifiers, because premise is in the conjunction. *)
+           (* TODO: after cleanup optimized in abd_simple, pass clean_ans
+              and remove cleanup here *)
+           let {cnj_typ=sb_ty; cnj_num=ans_num; cnj_so=_} =
+             combine_sbs q [prem.cnj_typ; concl_ty] in
+           let cnj_num = ans_num @ prem.cnj_num @ concl_num in
+           (* FIXME: need num state? *)
+           Some (br_vs, (sb_ty, NumS.satisfiable_exn cnj_num))
+         with Contradiction _ -> None)
+      verif_brs in
   (* TODO: could be optimized too. *)
   let neg_validate (vs, ans) =
     (* Returns the number of negative constraints not contradicted by
diff --git a/src/Abduction.mli b/src/Abduction.mli
index 4a86e32..8586d02 100644
--- a/src/Abduction.mli
+++ b/src/Abduction.mli
@@ -44,7 +44,7 @@ val num_neg_since : int ref
 val abd_fail_flag : bool ref
 val abd_timeout_flag : bool ref
 
-type t_validation = (Defs.VarSet.t * Terms.subst) list
+type t_validation = (Defs.VarSet.t * (Terms.subst * NumS.state)) list
 
 val abd_simple :
   Defs.quant_ops ->
diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml
index e520dfa..4028b79 100644
--- a/src/InvarGenTTest.ml
+++ b/src/InvarGenTTest.ml
@@ -202,7 +202,6 @@ let tests = "InvarGenT" >::: [
            test_case "flatten_pairs" ());
       "flatten_quadrs" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "flatten_quadrs" ());
       "flatten_septs" >::
@@ -440,12 +439,10 @@ let tests = "InvarGenT" >::: [
            test_case "liquid_bcopy" ());
       "liquid_bsearch-simpler" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_bsearch_simpler" ());
       "liquid_bsearch" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_bsearch" ());
       "liquid_bsearch-harder" >::
@@ -463,22 +460,18 @@ let tests = "InvarGenT" >::: [
            test_case "liquid_bsearch2_simpler2" ());
       "liquid_bsearch2" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_bsearch2" ());
       "liquid_bsearch2-harder1" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_bsearch2_harder1" ());
       "liquid_bsearch2-harder2" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_bsearch2_harder2" ());
       "liquid_bsearch2-harder3" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case ~test_annot:true "liquid_bsearch2_harder3" ());
       "liquid_bsearch2-harder4" >::
@@ -519,11 +512,11 @@ let tests = "InvarGenT" >::: [
            test_case "liquid_isort" ());
       "liquid_isort-harder" >::
         (fun () ->
+           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_isort_harder" ());
       "liquid_vecswap_simpler" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_vecswap_simpler" ());
       "liquid_vecswap" >::
@@ -532,6 +525,7 @@ let tests = "InvarGenT" >::: [
            test_case "liquid_vecswap" ());
       "liquid_isort-full" >::
         (fun () ->
+           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_isort_full" ());
       "liquid_tower_showposts" >::
@@ -544,7 +538,6 @@ let tests = "InvarGenT" >::: [
            test_case "liquid_tower_simpler" ());
       "liquid_tower_asserted" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_tower_asserted" ());
       "liquid_tower" >::
diff --git a/src/InvariantsTest.ml b/src/InvariantsTest.ml
index 78c3d7d..e91eda6 100644
--- a/src/InvariantsTest.ml
+++ b/src/InvariantsTest.ml
@@ -815,6 +815,7 @@ let rec plus =
 
   "binary plus asserted" >::
     (fun () ->
+       todo "FIXE";
        skip_if !debug "debug";
        test_case "binary plus"
 "datatype Binary : num
diff --git a/src/Joint.ml b/src/Joint.ml
index 2d2a685..474cee8 100644
--- a/src/Joint.ml
+++ b/src/Joint.ml
@@ -23,6 +23,7 @@ module type ABD_PARAMS = sig
   val abd_simple :
     args -> discard:discarded list ->
     validation:validation ->
+    validate:(VarSet.t -> answer -> unit) ->    
     neg_validate:(answer -> int) ->
     accu -> branch -> (accu * validation) option
   val extract_ans : accu -> answer
@@ -37,7 +38,8 @@ let debug_dep = ref 0
 
 module JointAbduction (P : ABD_PARAMS) = struct
 
-  let abd args ~discard (init_validation : P.validation) ~neg_validate
+  let abd args ~discard (init_validation : P.validation)
+      ~validate ~neg_validate
       init_acc brs =
     P.abd_fail_flag := false;
     let culprit = ref None
@@ -58,7 +60,7 @@ module JointAbduction (P : ABD_PARAMS) = struct
           (List.length aside_brs)
           (List.length more_brs) P.pr_branch br; *]*)
         match P.abd_simple args ~discard ~validation
-                ~neg_validate acc br with
+                ~validate ~neg_validate acc br with
         | Some (acc, validation) ->
           loop fails discard acc validation (br::done_brs)
             aside_brs more_brs
@@ -90,7 +92,7 @@ module JointAbduction (P : ABD_PARAMS) = struct
           ddepth (List.length discard) (List.length done_brs)
           (List.length aside_brs) P.pr_branch br; *]*)
         match P.abd_simple args ~discard ~validation
-                ~neg_validate acc br with
+                ~validate ~neg_validate acc br with
         | Some (acc, validation) ->
           check_aside fails best discard acc validation (br::done_brs)
             aside_brs
diff --git a/src/Joint.mli b/src/Joint.mli
index 9b1d403..43a2920 100644
--- a/src/Joint.mli
+++ b/src/Joint.mli
@@ -21,10 +21,12 @@ module type ABD_PARAMS = sig
   val abd_fail_timeout : int ref
   val abd_fail_flag : bool ref
   (** The variables passed to [validate] should be the variables of
-      the atom whose addition to the partial answer is being validated. *)
+      the atom whose addition to the partial answer is being
+      validated. Usually only one of [validation], [validate] is used. *)
   val abd_simple :
     args -> discard:discarded list ->
     validation:validation ->
+    validate:(VarSet.t -> answer -> unit) ->    
     neg_validate:(answer -> int) ->
     accu -> branch -> (accu * validation) option
   val extract_ans : accu -> answer
@@ -41,6 +43,7 @@ module JointAbduction (P : ABD_PARAMS) : sig
   val abd :
     P.args -> discard:P.discarded list ->
     P.validation ->
+    validate:(VarSet.t -> P.answer -> unit) ->
     neg_validate:(P.answer -> int) ->
     P.accu -> P.branch list -> P.accu
 end
diff --git a/src/NumS.ml b/src/NumS.ml
index 2dded4c..c945d36 100644
--- a/src/NumS.ml
+++ b/src/NumS.ml
@@ -9,7 +9,8 @@
 let early_num_abduction = ref (* false *)true
 let abd_rotations = ref (* 2 *)3(* 4 *)
 let abd_prune_at = ref (* 4 *)6(* 10 *)
-let abd_timeout_count = ref (* 500 *)1000(* 5000 *)(* 50000 *)
+let abd_timeout_count = ref (* 500 *)1000(* 5000 *)
+let abd_discard_param_only = ref (* false *)true
 let abd_fail_timeout_count = ref 20
 let aggressive_discard = ref (* false *)true
 let disjelim_rotations = ref 3
@@ -1330,7 +1331,7 @@ let choices ~cmp_v ~intro_cho_ineq optis suboptis =
 
 let implies ~cmp_v ~cmp_w uni_v eqs ineqs optis suboptis c_eqn c_ineqn
     c_optis c_suboptis =
-  (*[* Format.printf "implies: prem=@\n%a@\nconcl=@ %a@\n%a;@ %a@\n%!"
+  (*[* Format.printf "NumS.implies: prem=@\n%a@\nconcl=@ %a@\n%a;@ %a@\n%!"
     pr_state (eqs, ineqs, optis, suboptis)
     pr_eqnineqn (c_eqn, c_ineqn) pr_optis c_optis pr_suboptis c_suboptis; *]*)
   if c_optis=[] && c_suboptis=[]
@@ -1349,10 +1350,45 @@ let implies ~cmp_v ~cmp_w uni_v eqs ineqs optis suboptis c_eqn c_ineqn
          with Terms.Contradiction _ -> true)
       (choices ~cmp_v ~intro_cho_ineq:true optis suboptis)
 
-let implies_ans ~cmp_v ~cmp_w uni_v (eqs, ineqs, optis, suboptis)
+let implies_discard ~cmp_v ~cmp_w uni_v ~bvs (eqs, ineqs, optis, suboptis)
     (c_eqn, c_ineqn, c_optis, c_suboptis) =
-  implies ~cmp_v ~cmp_w uni_v eqs ineqs optis suboptis
-    c_eqn c_ineqn c_optis c_suboptis 
+  let eqs' =
+    if !abd_discard_param_only
+    then List.filter (fun (v, _) -> VarSet.mem v bvs) eqs
+    else eqs in
+  let ineqs' =
+    if !abd_discard_param_only
+    then List.filter (fun (v, _) -> VarSet.mem v bvs) ineqs
+    else ineqs in
+  let c_eqn' =
+    if !abd_discard_param_only
+    then List.filter
+        (function
+          | (v, _)::_, _, _ -> VarSet.mem v bvs
+          | _ -> false) c_eqn
+    else c_eqn in
+  let c_ineqn' =
+    if !abd_discard_param_only
+    then List.filter
+        (function
+          | (v, _)::_, _, _ -> VarSet.mem v bvs
+          | _ -> false) c_ineqn
+    else c_ineqn in
+  (* TODO: also for optis, suboptis *)
+  if c_eqn' = [] && c_ineqn' = [] then (
+    (*[* Format.printf "NumS.implies_discard: empty@\n%!"; *]*)
+    (* *)
+    (*[*let res =*]*)implies ~cmp_v ~cmp_w uni_v eqs ineqs optis suboptis
+      c_eqn c_ineqn c_optis c_suboptis
+      (*[* in Format.printf "NumS.implies_discard: implied? %b@\n%!" res;
+    res *]*)
+    (* *)
+    (* false *))
+  else
+    (*[*let res =*]*)implies ~cmp_v ~cmp_w uni_v eqs' ineqs' optis suboptis
+      c_eqn' c_ineqn' c_optis c_suboptis 
+      (*[* in Format.printf "NumS.implies_discard: implied? %b@\n%!" res;
+    res *]*)
 
 (* A streamlined portion of the [solve] algorithm dealing with
    inequalities. *)
@@ -1499,7 +1535,10 @@ let revert_uni ~cmp_v ~cmp_w ~uni_v ~bvs eqn =
   let rev_sb, _, _, _ =
     (* Do not use quantifiers. *)
     solve ~eqn ~cmp_v ~cmp_w uni_v in
-  List.filter (fun (v,_) -> uni_v v && not (VarSet.mem v bvs)) rev_sb
+  List.filter (fun (v, (vars, _, _)) ->
+      uni_v v && not (VarSet.mem v bvs) &&
+      not (List.exists (fun (v', _) ->
+          uni_v v' && not (VarSet.mem v' bvs)) vars)) rev_sb
 
 let revert_cst cmp_v uni_v eqn =
   let c_eqn, eqn = partition_map
@@ -1891,6 +1930,56 @@ let rename_w_atom sb = function
   | Opti_w (w1, w2) -> Opti_w (rename_w sb w1, rename_w sb w2)
   | Subopti_w (w1, w2) -> Subopti_w (rename_w sb w1, rename_w sb w2)
 
+let local_split ~cmp_v ~bvs ~xbvs eqn ineqn optis suboptis =
+  let leq x y =
+    let c = cmp_v x y in
+    if c = Same_quant then VarSet.mem x bvs else c <> Right_of in
+  let pick_var vs =
+    let res =
+      maximum ~leq (VarSet.elements vs) in
+    (*[* Format.printf "pick_var: vs=%a; res=%s@\n%!" pr_vars vs
+      (var_str res); *]*)
+    res in
+  let eqn = List.map
+      (fun w -> pick_var (fvs_w w), w) eqn
+  and ineqn = List.map
+      (fun w -> pick_var (fvs_w w), w) ineqn
+  and optis = List.map
+      (fun o -> pick_var (fvs_2w o), o) optis
+  and suboptis = List.map
+      (fun o -> pick_var (fvs_2w o), o) suboptis in
+  let split xvs = map_some
+      (fun (v, a) -> if VarSet.mem v xvs then Some a else None) in
+  List.map
+    (fun (x, xvs) ->
+       let x_eqn = split xvs eqn in
+       let x_ineqn = split xvs ineqn in
+       (*[* Format.printf
+         "local_split: x=%d; xvs=%a@\nx_eqn=%a@\nx_ineqn=%a@\n%!"
+       x pr_vars xvs pr_eqn x_eqn pr_ineqn x_ineqn; *]*)
+       x, (x_eqn, x_ineqn, split xvs optis, split xvs suboptis))
+    xbvs
+
+let subst_chi chi_sb pos_chi =
+  List.fold_left
+    (fun (acc_eqn, acc_ineqn, acc_optis, acc_suboptis)
+      (i, renaming) ->
+      let (eqn, ineqn, optis, suboptis) =
+        try List.assoc i chi_sb
+        with Not_found -> [], [], [], [] in
+      let eqn = List.map (rename_w renaming) eqn
+      and ineqn = List.map (rename_w renaming) ineqn
+      and optis = List.map
+          (fun (w1, w2) -> rename_w renaming w1, rename_w renaming w2)
+          optis
+      and suboptis = List.map
+          (fun (w1, w2) -> rename_w renaming w1, rename_w renaming w2)
+          suboptis in
+      eqn @ acc_eqn, ineqn @ acc_ineqn,
+      optis @ acc_optis, suboptis @ acc_suboptis)
+    ([], [], [], []) pos_chi
+
+(* Alternative approach, did not work well enough *)
 let subst_chi ~cmp_v ~bvs ~xbvs pos_chi a =
   let leq x y =
     (* let c = cmp_v x y in
@@ -1972,12 +2061,11 @@ let validate ~cmp_v ~cmp_w uni_v ~bvs ~xbvs validation a =
       validation;
     raise e
 
-
 (* We currently do not measure satisfiability of negative constraints. *)
 (* TODO: guess equalities between parameters. *)
 let abd_simple ~qcmp_v ~cmp_w
     ~orig_ren ~b_of_v ~upward_of cmp_v uni_v
-    ~bvs ~xbvs ~nonparam_vars ~discard ~validation
+    ~bvs ~xbvs ~nonparam_vars ~discard ~validation ~validate:_
     ~neg_validate:_
     skip (eqs_i, ineqs_i, optis_i, suboptis_i)
     (opti_lhs, (d_eqn, d_ineqn), (c_eqn, c_ineqn, c_optis, c_suboptis)) =
@@ -2081,7 +2169,7 @@ let abd_simple ~qcmp_v ~cmp_w
       "NumS.abd_simple: reverted c_eqn0=@ %a@\n%!"
       pr_eqn c_eqn0; *]*)
     (* 4 *)
-    let rec loop validation eq_trs
+    let rec loop valiation eq_trs
         eqs_acc0 ineqs_acc0 optis_acc suboptis_acc
         c0eqn c0ineqn c0optis c0suboptis =
       (*[* let ddepth = incr debug_dep; !debug_dep in *]*)
@@ -2099,7 +2187,7 @@ let abd_simple ~qcmp_v ~cmp_w
         | [], [], [], [] ->
           if (!skip > 0 && (decr skip; true))
           || List.exists
-               (implies_ans ~cmp_v ~cmp_w uni_v
+               (implies_discard ~cmp_v ~cmp_w uni_v ~bvs
                   (eqs_acc0, ineqs_acc0, optis_acc, suboptis_acc))
                (discard : (w list * w list * optis * suboptis) list)
           then
@@ -2148,7 +2236,7 @@ let abd_simple ~qcmp_v ~cmp_w
           "NumS.abd_simple: [%d] loop at:@\neqs=@ %a@\nineqs=@ %a@\n%!"
           ddepth pr_w_subst eqs_acc0 pr_ineqs ineqs_acc0;
         *]*)
-        loop validation eq_trs eqs_acc0
+        loop valiation eq_trs eqs_acc0
           ineqs_acc0 optis_acc suboptis_acc c0eqn c0ineqn
           c0optis c0suboptis)
       else
@@ -2223,7 +2311,7 @@ let abd_simple ~qcmp_v ~cmp_w
             ddepth pr_w_subst eqs_acc pr_ineqs ineqs_acc;
           *]*)
           (* (try                         *)
-          loop validation eq_trs eqs_acc ineqs_acc optis_acc suboptis_acc
+          loop valiation eq_trs eqs_acc ineqs_acc optis_acc suboptis_acc
             c0eqn c0ineqn c0optis c0suboptis in
       let try_trans_a a' =
         try
@@ -2404,10 +2492,10 @@ module NumAbd = struct
   let abd_simple
       {qcmp_v; cmp_w; cmp_v; uni_v; bvs; xbvs; nonparam_vars;
        b_of_v; orig_ren; upward_of}
-      ~discard ~validation ~neg_validate acc br =
+      ~discard ~validation ~validate ~neg_validate acc br =
     abd_simple ~qcmp_v ~cmp_w cmp_v ~orig_ren ~b_of_v ~upward_of
       uni_v ~bvs ~xbvs ~nonparam_vars
-      ~discard ~validation ~neg_validate 0 acc br
+      ~discard ~validation ~validate ~neg_validate 0 acc br
 
   let extract_ans ans = ans
 
@@ -2597,6 +2685,64 @@ let abd q ~bvs ~xbvs ?(orig_ren=empty_renaming) ?(b_of_v=empty_b_of_v)
       brs in
   let brs, validate_brs = List.split brs in
   (*[* Format.printf "NumS.abd: brs processing past merging@\n%!"; *]*)
+  (* let validate added_vs (eqs, ineqs, optis, suboptis) =
+    let chi_sb = local_split ~cmp_v:q.cmp_v ~bvs ~xbvs
+        (unsubst eqs) (unsolve ineqs) optis suboptis in
+    (*[* Format.printf
+      "NumS.abd-validate:@ eqs=%a@ ineqs=%a@ optis=%a@ suboptis=%a@ \
+       @\n%!"
+      pr_w_subst eqs pr_ineqs ineqs pr_optis optis pr_suboptis suboptis; *]*)
+    (* TODO: introduce use-site substitutions *)
+    try
+      List.iter
+        (fun (br_vs, brs_r, (_ (*[* as brs_n *]*)),
+              (_, chi_pos, _, (d_eqn, d_ineqn),
+               (c_eqn, c_ineqn, c_optis, c_suboptis))) ->
+          if chi_pos <> [] ||
+             VarSet.exists (fun v -> VarSet.mem v br_vs) added_vs
+          then
+            let prem_state =
+              (*[* Format.printf
+                "NumS.abd-validate: brs_r=%d; brs_n=%d\
+                 @\nd_eqn=%a@\nc_eqn=%a@\nd_ineqn=%a@\nc_ineqn=%a\
+                 @\nc_optis=%a@\nc_suboptis=%a@\n%!" !brs_r brs_n
+                pr_eqn d_eqn pr_eqn c_eqn pr_ineqn d_ineqn pr_ineqn c_ineqn
+                pr_optis c_optis pr_suboptis c_suboptis; *]*)
+              try
+                Right (solve ~eqs ~ineqs ~optis ~suboptis
+                         ~eqn:d_eqn ~ineqn:d_ineqn ~cmp_v ~cmp_w q.uni_v)
+              with Terms.Contradiction _ as e -> Left e in
+            match prem_state with
+            | Right (eqs,ineqs,optis,suboptis) ->
+              let u_eqn, u_ineqn, u_optis, u_suboptis as u =
+                subst_chi chi_sb chi_pos in
+              if VarSet.exists (fun v -> VarSet.mem v br_vs) added_vs ||
+                 VarSet.exists (fun v -> VarSet.mem v br_vs)
+                   (fvs_sep_w_formula u)
+              then
+                let (*[* br_eqs,br_ineqs,br_optis,br_suboptis *]*) _ =
+                  solve ~eqs ~ineqs
+                    ~eqn:(u_eqn @ c_eqn) ~ineqn:(u_ineqn @ c_ineqn)
+                    ~optis:(optis @ u_optis @ c_optis)
+                    ~suboptis:(suboptis @ u_suboptis @ c_suboptis)
+                    ~cmp_v ~cmp_w q.uni_v in
+                (*[* Format.printf
+                  "br_eqs=%a@\nbr_ineqs=%a@\nbr_optis=%a@\nbr_suboptis=%a@\n%!"
+                  pr_w_subst br_eqs pr_ineqs br_ineqs pr_optis br_optis
+                  pr_suboptis br_suboptis; *]*)
+                ()
+            | Left e ->
+              if !nodeadcode then (
+                decr brs_r;
+                if !brs_r <= 0 then (deadcode_flag := true; raise e)))
+        validate_brs;
+      (*[* Format.printf "NumS.abd-validate: passed@\n%!"; *]*)
+      List.iter (fun (_, brs_r, brs_n, _) -> brs_r := brs_n) validate_brs
+    with e ->
+      List.iter (fun (_, brs_r, brs_n, _) -> brs_r := brs_n) validate_brs;
+      raise e in*)
+  let validate _ _ = () in
+  (* Alternative approach not working well: *)
   let validation =
     map_some
       (fun (br_vs, brs_r, brs_n,
@@ -2660,7 +2806,7 @@ let abd q ~bvs ~xbvs ?(orig_ren=empty_renaming) ?(b_of_v=empty_b_of_v)
   let ans = JCA.abd
       {cmp_v; cmp_w; NumAbd.qcmp_v = q.cmp_v; orig_ren; b_of_v;
        upward_of; uni_v = q.uni_v; bvs; xbvs; nonparam_vars}
-      ~discard validation ~neg_validate ([], [], [], []) brs in
+      ~discard validation ~validate ~neg_validate ([], [], [], []) brs in
   [], elim_uni @ ans_to_num_formula ans