diff --git a/libexec/klab-prove b/libexec/klab-prove
index ea8573f8..5984bdc1 100755
--- a/libexec/klab-prove
+++ b/libexec/klab-prove
@@ -132,6 +132,7 @@ timeout "$TIMEOUT" "$KLAB_EVMS_PATH/deps/k/k-distribution/target/release/k/bin/k
   --smt_prelude "$KLAB_OUT/prelude.smt2" \
   --concrete-rules "$(join_by , ${concrete_rules[@]})" \
   --z3-tactic "(or-else (using-params smt :random-seed 3) (using-params smt :random-seed 2) (using-params smt :random-seed 1))" \
+  --deterministic-functions \
   "$target_spec" >"$STDOUT" 2>"$STDERR" & kprove_child=$!
 wait "$kprove_child"
 result=$?
diff --git a/resources/rules.k.tmpl b/resources/rules.k.tmpl
index b9ccb9f6..c3e4998b 100644
--- a/resources/rules.k.tmpl
+++ b/resources/rules.k.tmpl
@@ -315,10 +315,6 @@ rule ACCTCODE in SetItem( 1 )
     rule #if C #then (#if C #then B1 #else B2 #fi) -Int D #else (#if C #then B3 #else B4 #fi) -Int E #fi =>
          #if C #then B1 -Int D #else B4 -Int E #fi
 
-    // avoid nested #ifte
-    rule #if C1 #then A #else (B +Int #if C2 #then B2 #else B3 #fi) #fi =>
-         #if C1 #then A #else B #fi +Int #if (C2 andBool notBool C1) #then B2 #else 0 #fi +Int #if ((notBool C2) andBool (notBool C1)) #then B3 #else 0 #fi
-
    //simplify trivial #ifs
    rule #if C1 #then A #else B #fi => A
       requires A ==K B