diff --git a/include/kframework/lemmas/lemmas.k b/include/kframework/lemmas/lemmas.k index df81547319..463333247d 100644 --- a/include/kframework/lemmas/lemmas.k +++ b/include/kframework/lemmas/lemmas.k @@ -28,7 +28,7 @@ module LEMMAS [symbolic] rule chop(_V) true [simplification] rule X *Int Y true requires Y <=Int maxUInt256 /Int X [simplification] - rule #if B #then C +Int C1 #else C +Int C2 #fi => C +Int #if B #then C1 #else C2 #fi [simplification]jj + rule #if B #then C +Int C1 #else C +Int C2 #fi => C +Int #if B #then C1 #else C2 #fi [simplification] // ######################## // Set Reasoning diff --git a/include/kframework/serialization.md b/include/kframework/serialization.md index 945ffff9b1..aef4b67102 100644 --- a/include/kframework/serialization.md +++ b/include/kframework/serialization.md @@ -22,7 +22,7 @@ Address/Hash Helpers ```k syntax Int ::= keccak ( Bytes ) [function, total, injective, smtlib(smt_keccak)] - // ------------------------------------------------------------------------- + // -------------------------------------------------------------------------------- rule [keccak]: keccak(WS) => #parseHexWord(Keccak256(#unparseByteStack(WS))) [concrete] ```