Skip to content

Commit 1e36256

Browse files
committed
Add kore-rpc-booster results for test-remainder-predicates
1 parent 8246f99 commit 1e36256

File tree

7 files changed

+5831
-2
lines changed

7 files changed

+5831
-2
lines changed

booster/test/rpc-integration/resources/remainder-predicates.k

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,7 @@ module REMAINDER-PREDICATES
8585
/// two rules apply with SAT remainder predicate, //
8686
/// have to consider the remainder branch where X ==Int 0, //
8787
/// no further rules apply. //
88-
/// Aborts with boosted-dev; results in 2 branches in kore-rpc-booster. //
88+
/// Aborts with boosted-dev; results in 3 branches in kore-rpc-booster. //
8989
////////////////////////////////////////////////////////////////////////////////
9090
rule [test2-init]: <k> test2Init() => test2State1() ... </k>
9191
<int> _ => ?_X </int>
@@ -102,7 +102,7 @@ module REMAINDER-PREDICATES
102102
/// two rules apply with SAT remainder predicate, //
103103
/// have to consider the remainder branch where X ==Int 0, //
104104
/// but the are no further rules to apply. //
105-
/// Aborts with boosted-dev; results in 2 branches in kore-rpc-booster. //
105+
/// Aborts with boosted-dev; results in 3 branches in kore-rpc-booster. //
106106
////////////////////////////////////////////////////////////////////////////////
107107
rule [test3-init]: <k> test3Init() => test3State1() ... </k>
108108
<int> _ => ?_X </int>

booster/test/rpc-integration/test-remainder-predicates/response-test11.json

Lines changed: 481 additions & 0 deletions
Large diffs are not rendered by default.

booster/test/rpc-integration/test-remainder-predicates/response-test2.json

Lines changed: 936 additions & 0 deletions
Large diffs are not rendered by default.

booster/test/rpc-integration/test-remainder-predicates/response-test3.json

Lines changed: 936 additions & 0 deletions
Large diffs are not rendered by default.

booster/test/rpc-integration/test-remainder-predicates/response-test4.json

Lines changed: 1006 additions & 0 deletions
Large diffs are not rendered by default.

booster/test/rpc-integration/test-remainder-predicates/response-test5.json

Lines changed: 1065 additions & 0 deletions
Large diffs are not rendered by default.

booster/test/rpc-integration/test-remainder-predicates/response-test6.json

Lines changed: 1405 additions & 0 deletions
Large diffs are not rendered by default.

0 commit comments

Comments
 (0)