Solver's behavior is still symbols' name relevant, even if `random-seed` is set.

[chansey97]

Hi,

In the previous issue https://github.com/Z3Prover/z3/issues/5560, I found that z3's behavior is symbols' name relevant. That is, for the same program, safely replacing symbols' name may cause the behavior to be different.

The solution @NikolajBjorner suggested is setting random-seed to produce identical results.

Now I found a new example. That is even if random-seed is set, it is still symbols' name relevant.

The reproduction steps as follows:

1. Run ok.txt.

   $ z3 ok.txt smt.random_seed=1 smt.arith.solver=2
   sat
   sat
   sat
   sat
   sat
   sat
   sat
   unsat
   sat  <---- OK.

2. Open ok.txt, replace _w with _v.

3. Run the replaced file stuck.txt.

   $  z3 stuck.txt smt.random_seed=1 smt.arith.solver=2
   sat
   sat
   sat
   sat
   sat
   sat
   sat
   unsat 
   _   <---- Stuck!

Therefore, just symbol substitution causes the behavior to be different.

PS. The smt-lib-reference seemly does not require that symbol names and behavior must be irrelevant, but in general, we hope this good property.

My test environment:

z3-4.8.12-x64-win on windows 7.

[NikolajBjorner]

Yes, both random seed and symbol names influence search behavior.

The smt-lib reference cannot say anything about search behavior, it is solver specific and not something that can be standardized. It is either a missreading of the smtlib reference, poor wording, or miss-understanding regarding the reference to say anything about solver performance.