diff --git a/Cargo.lock b/Cargo.lock
index edacd57c..437233f3 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -4,9 +4,9 @@ version = 3
 
 [[package]]
 name = "aho-corasick"
-version = "1.1.1"
+version = "1.1.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ea5d730647d4fadd988536d06fecce94b7b4f2a7efdae548f1cf4b63205518ab"
+checksum = "b2969dcb958b36655471fc61f7e416fa76033bdd4bfed0678d8fee1e2d07a1f0"
 dependencies = [
  "memchr",
 ]
@@ -89,7 +89,7 @@ version = "0.66.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f2b84e06fc203107bfbad243f4aba2af864eb7db3b1cf46ea0a023b0b433d2a7"
 dependencies = [
- "bitflags 2.4.0",
+ "bitflags 2.4.1",
  "cexpr",
  "clang-sys",
  "lazy_static",
@@ -111,9 +111,9 @@ checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
 
 [[package]]
 name = "bitflags"
-version = "2.4.0"
+version = "2.4.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b4682ae6287fcf752ecaabbfcc7b6f9b72aa33933dc23a554d853aea8eea8635"
+checksum = "327762f6e5a765692301e5bb513e0d9fef63be86bbc14528052b1cd3e6f03e07"
 
 [[package]]
 name = "byteorder"
@@ -141,9 +141,9 @@ dependencies = [
 
 [[package]]
 name = "cargo_metadata"
-version = "0.18.0"
+version = "0.18.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fb9ac64500cc83ce4b9f8dafa78186aa008c8dea77a09b94cd307fd0cd5022a8"
+checksum = "2d886547e41f740c616ae73108f6eb70afe6d940c7bc697cb30f13daec073037"
 dependencies = [
  "camino",
  "cargo-platform",
@@ -518,9 +518,9 @@ dependencies = [
 
 [[package]]
 name = "linux-raw-sys"
-version = "0.4.9"
+version = "0.4.10"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "45786cec4d5e54a224b15cb9f06751883103a27c19c93eda09b0b4f5f08fefac"
+checksum = "da2479e8c062e40bf0066ffa0bc823de0a9368974af99c9f6df941d2c231e03f"
 
 [[package]]
 name = "lock_api"
@@ -672,9 +672,9 @@ checksum = "5b40af805b3121feab8a3c29f04d8ad262fa8e0561883e7653e024ae4479e6de"
 
 [[package]]
 name = "proc-macro2"
-version = "1.0.68"
+version = "1.0.69"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5b1106fec09662ec6dd98ccac0f81cef56984d0b49f75c92d8cbad76e20c005c"
+checksum = "134c189feb4956b20f6f547d2cf727d4c0fe06722b20a0eec87ed445a97f92da"
 dependencies = [
  "unicode-ident",
 ]
@@ -758,9 +758,9 @@ dependencies = [
 
 [[package]]
 name = "regex"
-version = "1.9.6"
+version = "1.10.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ebee201405406dbf528b8b672104ae6d6d63e6d118cb10e4d51abbc7b58044ff"
+checksum = "aaac441002f822bc9705a681810a4dd2963094b9ca0ddc41cb963a4c189189ea"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -770,9 +770,9 @@ dependencies = [
 
 [[package]]
 name = "regex-automata"
-version = "0.3.9"
+version = "0.4.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "59b23e92ee4318893fa3fe3e6fb365258efbfe6ac6ab30f090cdcbb7aa37efa9"
+checksum = "5011c7e263a695dc8ca064cddb722af1be54e517a280b12a5356f98366899e5d"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -781,9 +781,9 @@ dependencies = [
 
 [[package]]
 name = "regex-syntax"
-version = "0.7.5"
+version = "0.8.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dbb5fb1acd8a1a18b3dd5be62d25485eb770e05afb408a9627d14d451bae12da"
+checksum = "c08c74e62047bb2de4ff487b251e4a92e24f48745648451635cec7d591162d9f"
 
 [[package]]
 name = "rpds"
@@ -809,11 +809,11 @@ checksum = "8ba09476327c4b70ccefb6180f046ef588c26a24cf5d269a9feba316eb4f029f"
 
 [[package]]
 name = "rustix"
-version = "0.38.17"
+version = "0.38.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f25469e9ae0f3d0047ca8b93fc56843f38e6774f0914a107ff8b41be8be8e0b7"
+checksum = "745ecfa778e66b2b63c88a61cb36e0eea109e803b0b86bf9879fbc77c70e86ed"
 dependencies = [
- "bitflags 2.4.0",
+ "bitflags 2.4.1",
  "errno",
  "libc",
  "linux-raw-sys",
@@ -843,27 +843,27 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
 
 [[package]]
 name = "semver"
-version = "1.0.19"
+version = "1.0.20"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ad977052201c6de01a8ef2aa3378c4bd23217a056337d1d6da40468d267a4fb0"
+checksum = "836fa6a3e1e547f9a2c4040802ec865b5d85f4014efe00555d7090a3dcaa1090"
 dependencies = [
  "serde",
 ]
 
 [[package]]
 name = "serde"
-version = "1.0.188"
+version = "1.0.189"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cf9e0fcba69a370eed61bcf2b728575f726b50b55cba78064753d708ddc7549e"
+checksum = "8e422a44e74ad4001bdc8eede9a4570ab52f71190e9c076d14369f38b9200537"
 dependencies = [
  "serde_derive",
 ]
 
 [[package]]
 name = "serde_derive"
-version = "1.0.188"
+version = "1.0.189"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4eca7ac642d82aa35b60049a6eccb4be6be75e599bd2e9adb5f875a737654af2"
+checksum = "1e48d1f918009ce3145511378cf68d613e3b3d9137d67272562080d68a2b32d5"
 dependencies = [
  "proc-macro2",
  "quote",
diff --git a/binaries/summary_store.tar b/binaries/summary_store.tar
index 61183414..f0aa724e 100644
Binary files a/binaries/summary_store.tar and b/binaries/summary_store.tar differ
diff --git a/checker/src/abstract_value.rs b/checker/src/abstract_value.rs
index 7e7cdcf8..854ca428 100644
--- a/checker/src/abstract_value.rs
+++ b/checker/src/abstract_value.rs
@@ -649,8 +649,7 @@ impl AbstractValue {
     pub fn make_from(expression: Expression, expression_size: u64) -> Rc<AbstractValue> {
         if expression_size > k_limits::MAX_EXPRESSION_SIZE {
             if expression_size < u64::MAX {
-                trace!("expression {:?}", expression);
-                debug!("expression abstracted");
+                debug!("expression abstracted:  {:?}", expression);
             }
             // If the expression gets too large, refining it gets expensive and composing it
             // into other expressions leads to exponential growth. We therefore need to abstract
@@ -1256,6 +1255,22 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                         }
                     }
                 }
+                // [if c { a } else { b } && c] -> a
+                Expression::ConditionalExpression {
+                    condition,
+                    consequent,
+                    ..
+                } if condition.eq(&other) => {
+                    return consequent.clone();
+                }
+                // [if c { a } else { b } && !c] -> b
+                Expression::ConditionalExpression {
+                    condition,
+                    alternate,
+                    ..
+                } if condition.eq(&other.logical_not()) => {
+                    return alternate.clone();
+                }
                 _ => (),
             }
             match &other.expression {
@@ -2133,6 +2148,26 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                 }
             }
         }
+        // [if c {d} else { (if c {e} else {f}) join (if c {g} else {h}) }] -> if c {d} else { (f join h)}
+        if let Expression::Join { left, right } = &alternate.expression {
+            match (&left.expression, &right.expression) {
+                (
+                    Expression::ConditionalExpression {
+                        condition: c1,
+                        alternate: g,
+                        ..
+                    },
+                    Expression::ConditionalExpression {
+                        condition: c2,
+                        alternate: h,
+                        ..
+                    },
+                ) if c1.eq(c2) && c1.eq(self) => {
+                    return self.conditional_expression(consequent.clone(), g.join(h.clone()));
+                }
+                _ => {}
+            }
+        }
 
         // [if (if c { x } else { y }) { if c { a } else { b }} else { d }] ->
         // if c { if x { a } else { d } } else { if y { b } else { d } }
@@ -2159,6 +2194,28 @@ impl AbstractValueTrait for Rc<AbstractValue> {
             }
         }
 
+        // [if c { if (if c { a } else { b }) { x } else { y } } else { z }] -> if c { if a { x } else { y }} else {z}
+        if let Expression::ConditionalExpression {
+            condition: cab,
+            consequent: x,
+            alternate: y,
+        } = &consequent.expression
+        {
+            if let Expression::ConditionalExpression {
+                condition: c2,
+                consequent: a,
+                ..
+            } = &cab.expression
+            {
+                if self.eq(c2) {
+                    return self.conditional_expression(
+                        a.conditional_expression(x.clone(), y.clone()),
+                        alternate,
+                    );
+                }
+            }
+        }
+
         // if self { consequent } else { alternate } implies self in the consequent and !self in the alternate
         if !matches!(self.expression, Expression::Or { .. }) {
             if consequent.expression_size <= k_limits::MAX_EXPRESSION_SIZE / 10 {
@@ -4172,6 +4229,11 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                 return self.clone();
             }
 
+            // [(x && y) || x] -> x
+            if other.inverse_implies_not(self) {
+                return other.clone();
+            }
+
             // [x || !(x && y)] -> true, etc.
             if self.inverse_implies(&other) {
                 return Rc::new(TRUE);
@@ -4527,6 +4589,14 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                     return other;
                 }
 
+                // [(x && y) || !x] -> x && y
+                // [(x && y) || !y] -> x && y
+                (Expression::And { left: x, right: y }, Expression::LogicalNot { operand: xy })
+                    if x.eq(xy) || y.eq(xy) =>
+                {
+                    return self.clone();
+                }
+
                 // [x || (x && y)] -> x
                 // [y || (x && y)] -> y
                 (_, Expression::And { left: x, right: y }) if x.eq(self) || y.eq(self) => {
diff --git a/checker/src/environment.rs b/checker/src/environment.rs
index 4f8ad9cc..bc2d0fdc 100644
--- a/checker/src/environment.rs
+++ b/checker/src/environment.rs
@@ -353,7 +353,7 @@ impl Environment {
                                 // conditional on index == i
                                 let conditional_value = indices_are_equal
                                     .conditional_expression(value.clone(), v.clone());
-                                debug!("conditional_value {:?}", conditional_value);
+                                //debug!("conditional_value {:?}", conditional_value);
                                 self.strong_update_value_at(p.clone(), conditional_value);
                             }
                         }