Alpha-renaming causes convergence issues

[LeventErkok]

I have two SMT-Lib scripts:

• a.txt
• b.txt

These scripts are identical, except:

• The name of one recursive-function definition is different:
  • In a.txt, there is a function is called sbv.map_a99346
  • In b.txt, this very function is called sbv.map_532386
• Note that while the names are different, the definitions of these functions are identical.
• There are no other differences between the scripts.

When I run z3 on them, I get unsat immediately for a.smt2. But z3 goes into an infinite-loop with b.smt2.

I found that if I pass auto_config = false to z3, it converges on both of them quickly.

So, I do have a work-around. But If I could, I'd like to avoid using custom arguments:

1. I'm curious why a simple name change affects convergence. Any insights would be appreciated.
2. Is auto_config=false the right solution here? I'm concerned I might be giving up other features by setting this. Is there something less drastic I can do to avoid the problem?

[NikolajBjorner]

It is just unstable.
It also finishes quickly with a different random seed.

C:\z3\release>z3 b.txt /v:1 smt.random_seed=6 /st
(smt.seq :increase-length (sbv.map_532386[0] (seq.++ (seq.unit l1_s0!1) l1_s1!0)) 2)
(smt.seq :increase-length (sbv.map_532386[0] (seq.++ (sbv.reverse_8fc8f1[0] l1_s1!0) (seq.unit l1_s0!1))) 2)
(smt.seq :increase-length (sbv.reverse_8fc8f1[0] (seq.++ (seq.unit l1_s0!1) l1_s1!0)) 2)
unsat
(:added-eqs 3397
:arith-assert-diseq 5
:arith-assert-lower 188
:arith-assert-upper 229
:arith-bound-prop 4
:arith-eq-adapter 156
:arith-fixed-eqs 169
:arith-num-rows 67
:arith-offset-eqs 42
:arith-pivots 37
:arith-row-summations 76
:arith-tableau-max-columns 114
:arith-tableau-max-rows 67
:binary-propagations 690
:conflicts 58
:decisions 15
:del-clause 823
:max-generation 3
:max-memory 18.71
:memory 17.36
:mk-bool-var 2324
:mk-clause 828
:mk-clause-binary 538
:num-allocs 852655
:num-checks 2
:propagations 861
:quant-instantiations 125
:recfun-body-expansion 206
:recfun-case-expansion 54
:rlimit-count 171517
:seq-add-axiom 217
:seq-num-reductions 598
:time 0.03
:total-time 0.04)