0

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.

twhatm9
  • 27
  • 4
  • 1
    As far as z3 is concerned: If the counter-example is determined during the initial rewriting phase (i.e., before the actual SAT solving kicks in), then the counter-example won't depend on the seed. I can't speak for boogie, but I suspect a similar thing might be happening. Unless you've a "complicated enough" example for the SAT solver to make "random" choices, you'll get the same counter-example. Since you have "assert false," the solver immediately determines the system is `unsat` for any choice, and simply returns the very same counter-example. That'd be my (somewhat educated) guess. – alias May 26 '22 at 02:04
  • After some testing, I see this is indeed the case. "assert false" or some equality check is too simple to show any variance, but as soon as I change it to something like "assert Mod(i#0, LitInt(3)) == LitInt(0)" then the seed effectively changes the counterexample. It seems there doesn't exist a 'random_seed' prover option that is enacted before this 'rewriting phase', so I'll need to make sure my injected assertion is complicated enough yet not limiting to the domain. – twhatm9 May 26 '22 at 03:25

0 Answers0