Skip to content

Commit

Permalink
Fix typos, add link
Browse files Browse the repository at this point in the history
  • Loading branch information
geo2a committed Oct 29, 2024
1 parent 5db7f3c commit 9b41239
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 7 deletions.
10 changes: 5 additions & 5 deletions booster/test/rpc-integration/resources/remainder-predicates.k
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ module REMAINDER-PREDICATES
/// two rules apply with SAT remainder predicate, //
/// have to consider the remainder branch where X ==Int 0, //
/// but there are no further rules to apply. //
/// Aborts with boosted-dev; results in 3 branches in kore-rpc-booster. //
/// Aborts with booster-dev; results in 3 branches in kore-rpc-booster. //
////////////////////////////////////////////////////////////////////////////////
rule [test2-init]: <k> test2Init() => test2State1() ... </k>
<int> _ => ?_X </int>
Expand All @@ -104,7 +104,7 @@ module REMAINDER-PREDICATES
/// two rules apply with SAT remainder predicate, //
/// have to consider the remainder branch where X ==Int 0, //
/// no further rules apply. //
/// Aborts with boosted-dev; results in 3 branches in kore-rpc-booster. //
/// Aborts with booster-dev; results in 3 branches in kore-rpc-booster. //
////////////////////////////////////////////////////////////////////////////////
rule [test3-init]: <k> test3Init() => test3State1() ... </k>
<int> _ => ?_X </int>
Expand All @@ -126,7 +126,7 @@ module REMAINDER-PREDICATES
/// have to consider the remainder branch where X ==Int 0, //
/// one further regular rule applies, //
/// whose requires clause explicitly completes the space. //
/// Aborts with boosted-dev; results in 3 branches in kore-rpc-booster. //
/// Aborts with booster-dev; results in 3 branches in kore-rpc-booster. //
////////////////////////////////////////////////////////////////////////////////
rule [test4-init]: <k> test4Init() => test4State1() ... </k>
<int> _ => ?_X </int>
Expand All @@ -151,7 +151,7 @@ module REMAINDER-PREDICATES
/// have to consider the remainder branch where X ==Int 0, //
/// one rule at a lower priority applies unconditionally, which means that //
/// that the remainder is False. Rule test5-1-5 is unreachable. //
/// Aborts with boosted-dev; results in 3 branches in kore-rpc-booster. //
/// Aborts with booster-dev; results in 3 branches in kore-rpc-booster. //
////////////////////////////////////////////////////////////////////////////////
rule [test5-init]: <k> test5Init() => test5State1() ... </k>
<int> _ => ?_X </int>
Expand All @@ -176,7 +176,7 @@ module REMAINDER-PREDICATES
/// two hight-priorty rules apply with SAT remainder predicate, //
/// have to consider the remainder branch where X ==Int 0, //
/// two rules of lower priority appliy unconditionally. //
/// Aborts with boosted-dev; results in 4 branches in kore-rpc-booster. //
/// Aborts with booster-dev; results in 4 branches in kore-rpc-booster. //
////////////////////////////////////////////////////////////////////////////////
rule [test6-init]: <k> test6Init() => test6State1() ... </k>
<int> _ => ?_X </int>
Expand Down
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
# Tests for rewrite rule remainders in `kore-rpc-booster` and `kore-rpc-booster`
# Tests for rewrite rule remainders in `kore-rpc-booster` and `booster-dev`

See `../predicate-remainders.k`.
See [the related definition file](`../predicate-remainders.k`).

0 comments on commit 9b41239

Please sign in to comment.