CODEWITHSUNDEEP
randomz3boogie
twhatm9
twhatm9

Reputation: 27

Does random_seed affect the initial state of parameters in an implementation?

I'm interested in leveraging the random_seed attribute in order to have variety in the values returned by z3's counterexample. For instance, this implementation has 3 parameters of different types.

implementation {:random_seed N} Impl$$_module.__default.isOddLength(i#0: int, j#0: Seq Box, k#0: bool) returns (res#0: bool, $_reverifyPost: bool)
{
  var $_Frame: <beta>[ref,Field beta]bool;

  anon0:
    assume {:print "Impl", " | ", "Impl$$_module.__default.isOddLength", " | ", i#0, " | ", j#0, " | ", k#0} true;
    assume {:print "Types", " | ", "int", " | ", "Seq Box", " | ", "bool"} true;
    
    $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && read($Heap, $o, alloc) ==> false);
    $_reverifyPost := false;

    assert false;  // I injected this so I'll get a counterexample
...

No matter what I change the random_seed number N to, the initial state of the counterexample model always has the same values for i#0, j#0, and k#0.

*** STATE <initial>
  $_Frame -> 
  $_reverifyPost -> 
  $Heap -> T@U!val!4
  $Tick -> 
  i#0 -> 
  j#0 -> T@U!val!5
  k#0 -> 
  res#0 -> 
*** END_STATE

Is this due to implementation parameters being immutable? I understand I'm not allowed to havoc these parameters for the same reason. I'm wondering if this is also why z3 doesn't return values within the parameters' domains, no matter what random_seed is specified.

I'm willing to post more as needed.

Upvotes: 0

Views: 35

Answers (0)

Related Questions