diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 08320f46f8735f177ed979c0531b989c751010be..99497e15172f26286b0694fd2865e2643e1c7ee5 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -11,6 +11,7 @@ compile-coq:
   stage: compile
   script: ./scripts/ci-coq.sh
   artifacts:
+     expire_in: 1 week
      paths:
      - coq/
 
@@ -18,6 +19,7 @@ compile-hol:
   stage: compile
   script: ./scripts/ci-hol4.sh
   artifacts:
+     expire_in: 3 weeks
      paths:
      - hol4/
      - HOL4/
diff --git a/coq/SMTArith.v b/coq/SMTArith.v
index f65fe43f76f9b0dd7df3dbca40df264f353a191b..27b0b8bae295da614e45f169e00a1702f8d45909 100644
--- a/coq/SMTArith.v
+++ b/coq/SMTArith.v
@@ -11,6 +11,7 @@ Require Import Flover.RealRangeArith.
 
 Open Scope R.
 
+(* Restricted functions: cast, fma, and let are disallowed *)
 Inductive SMTArith :=
 | ConstQ (r: Q) : SMTArith
 | VarQ (x: nat) : SMTArith
@@ -20,7 +21,8 @@ Inductive SMTArith :=
 | TimesQ (e1 e2: SMTArith) : SMTArith
 | DivQ (e1 e2: SMTArith) : SMTArith.
 
-
+(* SMT of non-linear arithmetic:
+   comparisons of restricted functions, as well as usual boolean connectives *)
 Inductive SMTLogic :=
 | LessQ (e1 e2: SMTArith) : SMTLogic
 | LessEqQ (e1 e2: SMTArith) : SMTLogic
@@ -44,6 +46,7 @@ Definition getBound q :=
   | _ => None
   end.
 
+(* evaluation of restricted functions *)
 Inductive eval_smt (E: env) : SMTArith -> R -> Prop :=
 | VarQ_load x v : E x = Some v -> eval_smt E (VarQ x) v
 | ConstQ_eval r : eval_smt E (ConstQ r) (Q2R r)
@@ -57,6 +60,7 @@ Inductive eval_smt (E: env) : SMTArith -> R -> Prop :=
 | DivQ_eval e1 e2 v1 v2 :
     v2 <> 0 -> eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (DivQ e1 e2) (v1 / v2).
 
+(* semantics for SMT-statements *)
 Fixpoint eval_smt_logic (E: env) (q: SMTLogic) : Prop :=
   match q with
   | LessQ e1 e2 => exists v1 v2, eval_smt E e1 v1 /\ eval_smt E e2 v2 /\ v1 < v2
@@ -183,7 +187,8 @@ Proof.
   induction e; cbn; auto; now rewrite ?IHe, ?IHe1, ?IHe2.
 Qed.
 
-(* TODO handle Let and Cond *)
+(* comparison of functions and restricted functions as given above *)
+(* let's are handled separately *)
 Fixpoint smt_expr_eq (e: SMTArith) (e': expr Q) : bool :=
   match e', e with
   | Expressions.Const _ r', ConstQ r => Qeq_bool r r'
@@ -257,7 +262,6 @@ Proof.
     destruct m1; try discriminate.
     now apply IHe'.
   - cbn. congruence.
-  (* - cbn. congruence. *)
 Qed.
 
 Lemma eval_smt_expr E e v :
@@ -365,6 +369,7 @@ Proof.
   - Flover_compute. erewrite IHq1_1; eauto. erewrite IHq1_2; eauto.
 Qed.
 
+(* evaluation only depends on contained variables *)
 Lemma eval_smt_updEnv x v r E e :
   ~ (x ∈ varsSMT e) ->
   eval_smt E e v <-> eval_smt (updEnv x r E) e v.
@@ -446,6 +451,7 @@ Proof.
   - apply eval_smt_logic_updEnv; auto. intros ?. apply H. set_tac.
 Qed.
 
+(* define map of SMT-queries and unsatisfiability for them *)
 Definition usedQueries : Type := FloverMap.t (SMTLogic * SMTLogic).
 
 Definition unsat_queries qMap :=
@@ -458,6 +464,7 @@ Definition addVarConstraint (el: expr Q * intv) q :=
   | _ => q
   end.
 
+(* a precondition can be transformed into and equivalent SMT-statement *)
 Definition precond2SMT (P: precond) :=
   List.fold_right addVarConstraint (snd P) (FloverMap.elements (fst P)).
 
@@ -501,131 +508,32 @@ Proof.
       cbn in H. tauto.
 Qed.
 
-(* checker for precondition *)
-Fixpoint checkPrelist (lP: list (FloverMap.key * intv)) C q : bool :=
-  match lP, q with
-  | List.nil, _ => SMTLogic_eqb C q
-  | List.cons (Var _ x, (lo, hi)) lP', AndQ (LessEqQ (ConstQ lo') (VarQ y)) (AndQ (LessEqQ (VarQ z) (ConstQ hi')) q') => (x =? y) && (x =? z) && Qeq_bool lo lo' && Qeq_bool hi hi' && checkPrelist lP' C q'
-  | List.cons (Var _ x, _) _, _ => false
-  | List.cons el lP', _ => checkPrelist lP' C q
-  end.
-
-(*
-Lemma checkPrelist_LessQ lP C e1 e2 : checkPrelist lP C (LessQ e1 e2) = false.
-Proof.
-  induction lP as [|[e [lo hi]] l IHl]; auto.
-  destruct e; auto.
-Qed.
-
-Lemma checkPrelist_LessEqQ lP e1 e2 : checkPrelist lP (LessEqQ e1 e2) = false.
-Proof.
-  induction lP as [|[e [lo hi]] l IHl]; auto.
-  destruct e; auto.
-Qed.
-
-Lemma checkPrelist_EqualsQ lP e1 e2 : checkPrelist lP (EqualsQ e1 e2) = false.
-Proof.
-  induction lP as [|[e [lo hi]] l IHl]; auto.
-  destruct e; auto.
-Qed.
-
-Lemma checkPrelist_NotQ lP q : checkPrelist lP (NotQ q) = false.
-Proof.
-  induction lP as [|[e [lo hi]] l IHl]; auto.
-  destruct e; auto.
-Qed.
-
-Lemma checkPrelist_OrQ lP q1 q2 : checkPrelist lP (OrQ q1 q2) = false.
-Proof.
-  induction lP as [|[e [lo hi]] l IHl]; auto.
-  destruct e; auto.
-Qed.
-*)
-
-Definition checkPre (P: precond) q := checkPrelist (FloverMap.elements (fst P)) (snd P) q.
+Definition checkPre (P: precond) q := SMTLogic_eqb (precond2SMT P) q.
 
 Lemma checkPre_precond P : checkPre P (precond2SMT P) = true.
 Proof.
-  unfold precond2SMT, checkPre.
-  destruct P as [Piv C]. cbn.
-  induction (FloverMap.elements Piv) as [|[e [lo hi]] l IHl]; cbn. 
-  - apply SMTLogic_eqb_refl.
-  - destruct e; cbn; auto.
-    now rewrite Nat.eqb_refl, !Qeq_bool_refl, IHl.
+  unfold checkPre. apply SMTLogic_eqb_refl.
 Qed.
 
 Lemma checkPre_pre_smt E P q :
   checkPre P q = true ->
   eval_precond E P ->
   eval_smt_logic E q.
-Proof with try discriminate.
-  unfold checkPre, eval_precond, eval_preIntv.
-  destruct P as [Piv C]. cbn.
-  induction (FloverMap.elements Piv) as [|[e [lo hi]] l IHl] in q |- *.
-  - cbn. intros Heq [_ H]. now apply (SMTLogic_eqb_sound _ C).
-  - destruct e as [x| | | | | |].
-    all: try now (cbn; intros Heq [H1 H2]; apply IHl; auto).
-    cbn.
-    destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
-    destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
-    destruct e1 as [r| | | | | |]... destruct e2 as [|y| | | | |]...
-    destruct q2 as [? ?|? ?|? ?| |?|q1 q2|? ?]...
-    destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
-    destruct e1 as [|z| | | | |]... destruct e2 as [r'| | | | | |]...
-    intros chk [H HC].
-    apply andb_prop in chk as [chk chk0].
-    apply andb_prop in chk as [chk chk1].
-    apply andb_prop in chk as [chk chk2].
-    apply andb_prop in chk as [chk4 chk3].
-    apply beq_nat_true in chk4. apply beq_nat_true in chk3.
-    apply Qeq_bool_eq in chk2. apply Qeq_bool_eq in chk1.
-    rewrite <- chk3, <- chk4.
-    apply Qeq_sym in chk2. apply Qeq_sym in chk1.
-    (* assert (x ∈ fVars) as fx by (subst; set_tac; set_tac). *)
-    repeat split.
-    + destruct (H x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
-      exists (Q2R r), v. repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
-    + destruct (H x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
-      exists v, (Q2R r'). repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
-    + apply IHl; auto.
+Proof.
+  intros Heq HP.
+  apply (SMTLogic_eqb_sound _ _ _ Heq).
+  now apply pre_to_smt_correct.
 Qed.
 
-(*
 Lemma checkPre_smt_pre E P q :
-  checkPre P q = true -> eval_smt_logic E q -> eval_precond E P.
-Proof with try discriminate.
-  unfold P_intv_sound, checkPre.
-  induction (FloverMap.elements P) as [|[e [lo hi]] l IHl] in q |- *.
-  - destruct q; cbn; intros chk; try discriminate. tauto.
-  - destruct e as [x| | | | |];
-      try (intros chk H ? ? [?|?]; [discriminate| apply (IHl _ chk); auto]).
-    destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
-    destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
-    destruct e1 as [r| | | | | |]... destruct e2 as [|y| | | | |]...
-    destruct q2 as [? ?|? ?|? ?| |?|q1 q2|? ?]...
-    destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
-    destruct e1 as [|z| | | | |]... destruct e2 as [r'| | | | | |]...
-    cbn. intros chk H x' [lo' hi'] [eq|inl].
-    + apply andb_prop in chk. destruct chk as [chk chk0].
-      apply andb_prop in chk. destruct chk as [chk chk1].
-      apply andb_prop in chk. destruct chk as [chk chk2].
-      apply andb_prop in chk. destruct chk as [chk4 chk3].
-      apply beq_nat_true in chk4. apply beq_nat_true in chk3.
-      apply Qeq_bool_eq in chk2. apply Qeq_bool_eq in chk1.
-      destruct H as [[v1 [v2 [H1 [H2 H3]]]] [[v1' [v2' [H1' [H2' H3']]]] H]].
-      symmetry in chk4. symmetry in chk3.
-      assert (x' = x) by congruence.
-      assert (lo' = lo) by congruence.
-      assert (hi' = hi) by congruence.
-      subst.
-      inversion H1. inversion H2. inversion H1'. inversion H2'.
-      assert (v2 = v1') by congruence.
-      subst. cbn. rewrite (Qeq_eqR _ _ chk2). rewrite (Qeq_eqR _ _ chk1).
-      exists v1'. repeat split; auto.
-    + apply andb_prop in chk. destruct chk as [chk chk0].
-      apply (IHl _ chk0); tauto.
+  checkPre P q = true ->
+  eval_smt_logic E q ->
+  eval_precond E P.
+Proof.
+  intros Heq Hq.
+  apply smt_to_pre_correct.
+  now apply (SMTLogic_eqb_sound _ _ _ Heq).
 Qed.
-*)
 
 Lemma precond_bound_correct E P preQ bound :
   eval_precond E P ->
@@ -638,6 +546,7 @@ Proof.
   eapply checkPre_pre_smt; eauto.
 Qed.
 
+(* unsat queries of appropriate form yield bounds *)
 Lemma RangeBound_low_sound E P preQ e r Gamma v :
   eval_precond E P ->
   checkPre P preQ = true ->
@@ -650,7 +559,7 @@ Proof.
   apply Rnot_lt_le. intros B.
   apply H2. eapply precond_bound_correct; eauto.
   split; cbn; auto.
-  do 2 eexists. repeat split; first [eassumption | constructor].
+  exists v, (Q2R r). repeat split; auto. constructor.
 Qed.
 
 Lemma RangeBound_high_sound E P preQ e r Gamma v :
@@ -665,5 +574,5 @@ Proof.
   apply Rnot_lt_le. intros B.
   apply H2. eapply precond_bound_correct; eauto.
   split; cbn; auto.
-  do 2 eexists. repeat split; first [eassumption | constructor].
+  exists (Q2R r), v. repeat split; auto. constructor.
 Qed.
diff --git a/coq/SMTValidation.v b/coq/SMTValidation.v
index 1b0ca408c1962a492e0c3ac4803a2fab10e10ed9..ca1bdf81a58e05dc6faafd79206f77e3f5fe0712 100644
--- a/coq/SMTValidation.v
+++ b/coq/SMTValidation.v
@@ -17,6 +17,7 @@ From Flover
      Require Export IntervalArithQ IntervalArith SMTArith ssaPrgs
      RealRangeArith.
 
+(* let_env is used to store the mapping [x |-> f] when encountering function (let x := f in g) *)
 Definition let_env := nat -> option (expr Q).
 
 Definition lets_sound L E Gamma :=
@@ -40,9 +41,9 @@ Fixpoint inlineLets (L: let_env) (e: expr Q) :=
   | Fma e1 e2 e3 => Fma (inlineLets L e1) (inlineLets L e2) (inlineLets L e3)
   | Downcast m e' => Downcast m (inlineLets L e')
   | Let m x e1 e2 => Let m x (inlineLets L e1) (inlineLets L e2)
-  (* | Cond e1 e2 e3 => Cond (inlineLets L e1) (inlineLets L e2) (inlineLets L e3) *)
   end.
 
+(* inlineLets preserves evaluation for reasonable let_env *)
 Lemma inlineLets_sound L E Gamma inVars outVars e v :
   lets_sound L E Gamma ->
   (forall x e, L x = Some e -> NatSet.Subset (NatSet.add x (freeVars e)) inVars) ->
@@ -112,19 +113,6 @@ Proof.
           apply H4. eapply LfVars_valid; eauto.
           set_tac. }
       * now extended_ssa.
-            (*
-  - inversion H; subst.
-    + assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
-      inversion ssa_e; subst.
-      subst.
-      assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
-      subst. eapply Cond_then; eauto.
-    + assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
-      inversion ssa_e; subst.
-      subst.
-      assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
-      subst. eapply Cond_else; eauto.
-*)
 Qed.
 
 Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) P L :=
@@ -141,6 +129,7 @@ Definition tightenUpperBound (e: expr Q) (hi: Q) (q: SMTLogic) P L :=
   | _ => hi
   end.
 
+(* try to tighten the given interval using correct encoded queries *)
 Definition tightenBounds (e: expr Q) (iv: intv) (qMap: usedQueries) P L :=
   match FloverMap.find e qMap with
   | None => iv
@@ -204,6 +193,7 @@ Proof.
   exact H.
 Qed.
 
+(* tightening using appropriate unsat queries is sound *)
 Lemma tightenBounds_sound E Gamma e v iv qMap P L :
   eval_precond E P ->
   (forall ql qh, FloverMap.find e qMap = Some (ql, qh) ->
@@ -220,6 +210,8 @@ Proof.
     intros. edestruct unsatQ; eauto.
 Qed.
 
+(* the final validator is essentially the interval arithmetic validator,
+   except that in each step 'tightenBounds' is applied *)
 Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
          (Q: usedQueries) L (validVars: NatSet.t) : bool :=
   match FloverMap.find e A with
@@ -319,23 +311,11 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
            | _, _, _ => false
            end
          else false
-       (* | Cond f1 f2 f3 => false *)
-       (*
-       if ((validSMTIntervalbounds f1 A P validVars) &&
-           (validSMTIntervalbounds f2 A P validVars) &&
-           (validSMTIntervalbounds f3 A P validVars))
-       then
-         match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with
-         | Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
-           let new_iv := (* TODO *) in
-           isSupersetIntv new_iv intv
-         | _, _, _ => false
-         end
-       else false
-            *)
        end
   end.
 
+(* soundness proof is essentially the same as the one for interval arithmetic,
+   except in each step 'tightenBounds_sound' is applied *)
 Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: precond)
         (Q: usedQueries) L fVars dVars outVars (E: env) Gamma :
   unsat_queries Q ->
diff --git a/coq/SubdivsChecker.v b/coq/SubdivsChecker.v
index e61e667f912b4ce61a5ddcbf80b8c3396af89e9f..dea086e8e8f2aaf2c112b68beff442d89b3d4789 100644
--- a/coq/SubdivsChecker.v
+++ b/coq/SubdivsChecker.v
@@ -6,6 +6,7 @@ From Flover
 
 Require Import List FunInd Sorting.Permutation Sorting.Mergesort Orders.
 
+(* define relation on the analysis results, such that validity carries over *)
 Fixpoint resultLeq e (A1 A2: analysisResult) :=
   match e with
   | Unop _ e1 | Downcast _ e1 => resultLeq e1 A1 A2
@@ -56,6 +57,7 @@ Proof.
   - apply (reflect_iff _ _ (Z.leb_spec0 _ _)). auto.
 Qed.
 
+(* validRanges carries over *)
 Lemma resultLeq_range_sound e A1 A2 E Gamma :
   resultLeq e A1 A2 = true ->
   validRanges e A1 E Gamma ->
@@ -145,6 +147,7 @@ Proof.
       repeat split; auto; lra.
 Qed.
 
+(* validErrorBounds carries over *)
 Lemma resultLeq_error_sound e A1 A2 E1 E2 Gamma :
   resultLeq e A1 A2 = true ->
   validErrorBounds e E1 E2 A1 Gamma ->
@@ -268,7 +271,6 @@ Proof.
       lra.
 Qed.
 
-(* TODO: maybe put this somewhere else *)
 Lemma approxEnv_empty_dVars A1 A2 Gamma fVars dVars E1 E2 :
   NatSet.Empty dVars ->
   approxEnv E1 Gamma A1 fVars dVars E2 ->
@@ -281,6 +283,7 @@ Proof.
   - exfalso. eapply He. set_tac.
 Qed.
 
+(* run checker on subdomain and check the above relation *)
 Definition checkSubdivsStep e absenv defVars Gamma (PAQ: precond * analysisResult * usedQueries) :=
   match PAQ with
   | (P, A, Q) =>
@@ -318,38 +321,15 @@ Proof.
   now apply andb_true_iff in H as [H1 H2].
 Qed.
 
-Fixpoint coverIntv iv intvs :=
-  match intvs with
-  | nil => false
-  | intv :: nil => isSupersetIntv iv intv
-  | intv :: intvs =>
-    Qleb (ivlo intv) (ivlo iv) && coverIntv (ivhi intv, ivhi iv) intvs
-  end.
-
-Lemma coverIntv_sound iv intvs v :
-  coverIntv iv intvs = true ->
-  (Q2R (ivlo iv) <= v <= Q2R (ivhi iv))%R ->
-  exists intv, In intv intvs /\ (Q2R (ivlo intv) <= v <= Q2R (ivhi intv))%R.
-Proof.
-  induction intvs as [|intv0 intvs] in iv |- *; [intros H; discriminate H|].
-  destruct intvs as [|intv1 intvs]; cbn; intros H Hin.
-  - exists intv0. split; auto. andb_to_prop H. canonize_hyps. cbn in *. lra.
-  - destruct (Rle_or_lt v (Q2R (ivhi intv0))) as [Hle|Hlt].
-    + andb_to_prop H.
-      canonize_hyps.
-      exists intv0. split; cbn; auto.
-      cbn in *. lra.
-    + andb_to_prop H.
-      destruct (IHintvs (ivhi intv0, ivhi iv)) as [intv [inl Hin1]]; eauto.
-      cbn in *. lra.
-Qed.
-
+(* remove the preconds 'P' from 'Ps' that have contraint 'iv' for input 'x';
+   from those 'P' remove this constraint and collect them in 'sl';
+   other 'P' are collected in 'rest' *)
 Fixpoint getSlice x iv Ps :=
   match Ps with
   | nil => (nil, nil)
   | P :: Ps' =>
     match P with
-    | nil => (nil, Ps) (* fail *)
+    | nil => (nil, Ps)
     | (e, ivE) :: P' =>
       if FloverMapFacts.P.F.eqb (Var Q x) e && isSupersetIntv iv ivE then
            let (sl, rest) := getSlice x iv Ps' in (P' :: sl, rest)
@@ -370,6 +350,7 @@ Proof with try now injection 1; intros; subst.
   cbn. now rewrite <- IHPs.
 Qed.
 
+(* from precond 'P' in slice 'sl', we can construct precond in Ps *)
 Lemma getSlice_sound x iv Ps sl rest :
   getSlice x iv Ps = (sl, rest) ->
   forall P, In P sl ->
@@ -388,6 +369,7 @@ Proof with try now injection 1; intros; subst.
   - edestruct IHPs as [ivx [inPs sub]]; eauto.
 Qed.
 
+(* 'rest' is subset 'Ps' *)
 Lemma getSlice_rest_sound x iv Ps sl rest :
   getSlice x iv Ps = (sl, rest) ->
   forall P, In P rest -> In P Ps.
@@ -401,6 +383,7 @@ Proof with try now injection 1; intros; subst.
   right. eapply IHPs; eauto.
 Qed.
 
+(* for 'P' in 'Ps', there are only the two cases above *)
 Lemma getSlice_complete x iv Ps sl rest :
   getSlice x iv Ps = (sl, rest) ->
   forall P, In P Ps ->
@@ -421,42 +404,7 @@ Proof with try now injection 1; intros; subst; auto.
     right. exists P1, ivx. split; auto. now constructor 2.
 Qed.
 
-(*
-Function checkDim cov x iv Ps {measure length Ps} :=
-  match Ps with
-  | nil => false
-  | P :: _ =>
-    match FloverMap.find (Var Q x) P with
-    | Some ivx =>
-      let (b, rest) := getSlice_aux x ivx Ps in
-      let covb := cov b in
-      covb && match rest with
-              | nil => isSupersetIntv iv ivx
-              | _ => checkDim cov x (snd ivx, snd iv) rest
-              end
-    | None => false
-    end
-  end.
-intros cov x iv Ps P Ps' HPs ivx Hfind b rest P' rest' Hrest.
-rewrite <- Hrest.
-rewrite <- HPs at 2.
-cbn.
-unfold addToSlice.
-rewrite Hfind.
-unfold isSupersetIntv, Qleb, Qle_bool.
-rewrite !Z.leb_refl.
-rewrite <- HPs.
-cbn.
-destruct (getSlice_aux x ivx Ps') eqn:Heq.
-apply getSlice_aux_sound in Heq.
-clear Hrest rest'.
-injection 1; intros; subst.
-cbn.
-rewrite Heq, app_length.
-apply le_lt_n_Sm, le_plus_r.
-Defined.
-*)
-
+(* checks all slices of variable 'x' with function 'cov' *)
 Function checkDim cov x iv Ps {measure length Ps} :=
   match Ps with
   | nil => false
@@ -488,6 +436,7 @@ rewrite app_length.
 apply le_lt_n_Sm, le_plus_r.
 Defined.
 
+(* check the slices of var 'x' recursively *)
 Fixpoint covers (P: list (expr Q * intv)) Ps :=
   match P with
   | nil => match Ps with nil::nil => true | _ => false end
@@ -496,6 +445,7 @@ Fixpoint covers (P: list (expr Q * intv)) Ps :=
   | _ :: P => false
   end.
 
+(* a input has to be in one subdomain if subdomains cover global domain *)
 Lemma covers_sound P Ps E :
   covers P Ps = true ->
   eval_preIntv E P ->
@@ -578,6 +528,8 @@ Proof.
         eapply IHP; eauto.
 Qed.
 
+(* order the subdomains lexicographically, such that the above algorithm
+   works as intended *)
 Module PrecondOrder <: TotalLeBool.
 
   Definition t := list (expr Q * intv).
@@ -610,11 +562,10 @@ Definition checkPreconds (subdivs: list precond) (P: precond) :=
   let Piv := FloverMap.elements (fst P) in
   let Ps := map (fun P => FloverMap.elements (fst P)) subdivs in
   let S_qs := map snd subdivs in
-  (* Check that join of the preconditions for the subdivisions
-     covers the global precondition *)
+  (* check that subdomains cover global domain *)
   covers Piv (sort Ps) &&
-         (* Check that additional constraints encoded by Daisy agree
-            for each subdivision *)
+         (* check that additional constraints for the subdomain agree
+            with the one for the global domain *)
          forallbTailrec (fun q => SMTLogic_eqb q (snd P)) S_qs.
 
 Lemma checkPreconds_sound (subdivs: list precond) E P :
@@ -654,18 +605,41 @@ Proof.
   apply in_map_iff; eauto.
 Qed.
 
-(** Interval subdivisions checking function **)
+(* check for emptiness as witnessed by a suitable query *)
+Definition isNonEmptySubdiv e (S: precond * analysisResult * usedQueries) :=
+  match S with
+  | (P, A, Q) => match FloverMap.find e Q with
+                | Some (q, _) => negb (checkPre P q)
+                | None => true
+                end
+  end.
+
+Lemma isNonEmptySubdiv_sound E e P A Q :
+  eval_precond E P ->
+  unsat_queries Q ->
+  isNonEmptySubdiv e (P, A, Q) = true.
+Proof.
+  intros HP HQ. cbn.
+  destruct (FloverMap.find e Q) as [[q1 q2] |] eqn: Hfind; auto.
+  destruct (checkPre P q1) eqn: H; auto.
+  exfalso. destruct (HQ E e q1 q2) as [HnP _]; auto.
+  apply HnP.
+  eapply checkPre_pre_smt; eauto.
+Qed.
+
+(** interval subdivision checker function **)
 Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
            (P: precond) subdivs (defVars: FloverMap.t  mType) Gamma :=
   validSSA e (preVars P) &&
            checkPreconds (map (fun S => match S with (P, _, _) => P end) subdivs) P &&
-           checkSubdivs e absenv subdivs defVars Gamma.
+           (* check results only for non-empty domains *)
+           checkSubdivs e absenv (filter (isNonEmptySubdiv e) subdivs) defVars Gamma.
 
 Definition queriesInSubdivs (subdivs: list (precond * analysisResult * usedQueries)) :=
   map (fun S => match S with (_, _, Q) => Q end) subdivs.
 
 (**
-   Soundness proof for the interval subdivs checker.
+   soundness proof for the interval subdivision checker
 **)
 Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P subdivs defVars Gamma:
   forall (E1 E2: env) DeltaMap,
@@ -680,17 +654,6 @@ Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P subdivs de
     validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\
     validErrorBounds e E1 E2 absenv Gamma /\
     validFPRanges e E2 Gamma DeltaMap.
-  (*
-    exists Gamma,
-      approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
-      exists iv err vR vF m,
-        FloverMap.find e absenv = Some (iv, err) /\
-        eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) vR REAL /\
-        eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m /\
-        (forall vF m,
-            eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
-            (Rabs (vR - vF) <= Q2R err))%R.
-*)
 Proof.
   intros * deltas_matched approxEnv P_valid unsat_qs valid_typeMap chk.
   apply andb_prop in chk as [chk valid_subdivs].
@@ -700,7 +663,11 @@ Proof.
   { eapply validSSA_eq_set; eauto. eapply checkPreconds_preVars; eauto. }
   apply in_map_iff in in_subdivs as [[[P2 A] Qmap] [Heq in_subdivs]].
   cbn in Heq; subst.
-  pose proof (checkSubdivs_sound  e _ _ _ _ _ _ _ valid_subdivs in_subdivs) as [range_err_check A_leq].
+  assert (In (P1, A, Qmap) (filter (isNonEmptySubdiv e) subdivs)) as in_nonempty_subdivs.
+  { apply filter_In. split; auto.
+    eapply isNonEmptySubdiv_sound; eauto.
+    apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
+  pose proof (checkSubdivs_sound  e _ _ _ _ _ _ _ valid_subdivs in_nonempty_subdivs) as [range_err_check A_leq].
   assert (ResultChecker e A P1 Qmap defVars Gamma = true) as res_check
     by (unfold ResultChecker; now rewrite valid_ssa', range_err_check).
   eapply approxEnv_empty_dVars in approxEnv; eauto.
@@ -708,28 +675,3 @@ Proof.
   { apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
   repeat split; eauto using resultLeq_range_sound, resultLeq_error_sound.
 Qed.
-
-(*
-  exists Gamma; intros approxE1E2.
-  assert (approxEnv E1 (toRExpMap Gamma) A (freeVars e) NatSet.empty E2) as approxE1E2'
-      by (eapply approxEnv_empty_dVars; eauto).
-  assert (validRanges e A E1 (toRTMap (toRExpMap Gamma))) as validRange.
-  { edestruct result_checking_sound; eauto; [| intuition].
-    apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
-  assert (validErrorBounds e E1 E2 A Gamma) as Hsound.
-  { edestruct result_checking_sound; eauto; [| intuition].
-    apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
-  eapply validRanges_single in validRange.
-  destruct validRange as [iv [err [vR [Hfind [eval_real validRange]]]]].
-  eapply validErrorBoundsRec_single in Hsound; eauto.
-  destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto.
-  destruct (resultLeq_sound _ _ _ A_leq) as [iv1 [err1 [iv2 [err2 H]]]].
-  destruct H as [F1 [F2 [sub err_leq]]].
-  exists iv2, err2, vR, vF, mF; repeat split; auto.
-  assert (err = err1) by congruence; subst.
-  apply Qle_Rle in err_leq.
-  intros vF0 m Heval.
-  specialize (err_bounded vF0 m Heval).
-  lra.
-Qed.
-*)