rules.k: remove nested #ifte simplification

It clashes with this rule in domains.k: ```k rule #if C:Bool #then _ #else B2::K #fi => B2 requires notBool C ```
dapphub · Apr 8, 2020 · bf46cea · bf46cea
1 parent 853e470
commit bf46cea
Showing 1 changed file with 0 additions and 4 deletions.
diff --git 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