Влияет ли random_seed на начальное состояние параметров в реализации?

Question

Я заинтересован в использовании атрибута random_seed для разнообразия значений, возвращаемых контрпримером z3. Например, эта реализация имеет 3 параметра разных типов.

      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
...

Независимо от того, на что я изменяю число random_seed N, начальное состояние модели контрпримера всегда имеет одни и те же значения для i#0, j#0 и 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

Это связано с тем, что параметры реализации неизменны? Я понимаю, что мне не разрешено нарушать эти параметры по той же причине. Мне интересно, является ли это также причиной того, что z3 не возвращает значения в пределах доменов параметров, независимо от того, что указано random_seed.

Я готов публиковать больше по мере необходимости.