Branching on a range of integers in K?

Question

I read in the documentation that one can write a rule

syntax Exp ::= randBounded(Int, Int)
rule randBounded(M, N) => I
  requires M <=Int I andBool I <=Int N
  [unboundVariables(I)]

I would like randBounded(4,6) to return some random integer. However, when I try it, it returns an integer V0 and sets constraints V0 <=Int 10 ==K true.

Is there a way, instead, to generate explicit branches for every integer in a range?

e.g. I would like to have --search produce 3 configurations: One for each Integer 4, Integer 5 and Integer 6.

Answer 1

Unfortunately, the expansion you suggest is not possible with --search so you cannot get the exact three configurations. However, if you don't actually need those precise configurations, but instead want to be able to reason on their properties, performing (symbolic) execution (using the haskell backend) using this rule somehow comprises all three configurations.