Minor change to the name of function goes from unsat to timeout

[asr]

I'm using the tptp2X program from the TPTP world for translating some problems from TPTP to SMT-LIB2.

In the following problem (sorry, I couldn't find a smaller example and please keep in mind that this problem was automatically generated)

$ cat ok.smt2
;------------------------------------------------------------------------------
(set-logic UFNIRA)

(declare-sort smt_individual 0)

; kp1__2_type
(declare-fun kp1_ (smt_individual smt_individual) Bool)

; kp4__5_type
(declare-fun kp4_ (smt_individual smt_individual smt_individual smt_individual smt_individual) Bool)

; cA_0_type
(declare-fun cA () smt_individual)

; cN_0_type
(declare-fun cN () smt_individual)

; n43_2_type
(declare-fun n43 (smt_individual smt_individual) smt_individual)

; succ_1_type
(declare-fun succ (smt_individual) smt_individual)

; zero_0_type
(declare-fun zero () smt_individual)

; n44_69078460
(assert
    (forall ((?A smt_individual)) (= (n43 zero ?A) ?A) )
)

; n50_69078460
(assert
    (forall ((?A smt_individual))
    (forall ((?B smt_individual)) (= (n43 (succ ?A) ?B) (succ (n43 ?A ?B))) ) )
)

; n74_69078460
(assert
    (forall ((?A smt_individual))
    (forall ((?B smt_individual))
    (forall ((?C smt_individual))
      (=> (kp1_ cN ?A)
          (=> (kp1_ cN ?B)
              (=> (kp1_ cN ?C)
                  (forall ((?D smt_individual))
                    ( = (kp4_ cA ?A ?B ?C ?D)
                        (= (n43 (n43 ?D ?B) ?C) (n43 ?D (n43 ?B ?C))) ) ) ) ) ) ) ) )
)

;----This is the conjecture with negated conjecture; n78_69078460
(assert
    (not (forall ((?A smt_individual))
        (forall ((?B smt_individual))
        (forall ((?C smt_individual))
          (=> (kp1_ cN ?A)
              (=> (kp1_ cN ?B)
                  (=> (kp1_ cN ?C)
                      (kp4_ cA ?A ?B ?C zero) ) ) ) ) ) ) )
)

(check-sat)
;------------------------------------------------------------------------------

using Z3 4.4.1 I got the expected unsat

$ z3 -T:10 ok.smt2
unsat

but by renaming the n43 function to n_43 I got a timeout

$ z3 -T:10 bad.smt2
timeout

$ diff ok.smt2 bad.smt2 
18,19c18,19
< ; n43_2_type
< (declare-fun n43 (smt_individual smt_individual) smt_individual)

---
> ; n_43_2_type
> (declare-fun n_43 (smt_individual smt_individual) smt_individual)
29c29
<     (forall ((?A smt_individual)) (= (n43 zero ?A) ?A) )

---
>     (forall ((?A smt_individual)) (= (n_43 zero ?A) ?A) )
35c35
<     (forall ((?B smt_individual)) (= (n43 (succ ?A) ?B) (succ (n43 ?A ?B))) ) )

---
>     (forall ((?B smt_individual)) (= (n_43 (succ ?A) ?B) (succ (n_43 ?A ?B))) ) )
48c48
<                         (= (n43 (n43 ?D ?B) ?C) (n43 ?D (n43 ?B ?C))) ) ) ) ) ) ) ) )

---
>                         (= (n_43 (n_43 ?D ?B) ?C) (n_43 ?D (n_43 ?B ?C))) ) ) ) ) ) ) ) )

[wintersteiger]

Confirmed, reproducible. This kind of bug is hard to track down, so it might take some time until we get a solution for this.

[asr]

Thanks for reproducing the issue. Why wasn't the bug label add to the issue?

[wintersteiger]

Because it's a performance issue, not a soundness issue, but I can add the label if you like.

[NikolajBjorner]

The same can be obtained by changing the random seed:
z3 bad.smt2 smt.random_seed=7

[asr]

The same can be obtained by changing the random seed:
z3 bad.smt2 smt.random_seed=7

What does it mean?

[wintersteiger]

It means that small changes to the input can have a big impact on the runtime, which is unavoidable and expected. However, in this specific case it seems like it's only the name of the variable that seems to make the difference, which is something we should at least look at before dismissing it.

[asr]

Thanks for the explanation.

[asr]

The issue is fixed in Z3 4.5.0. Thanks!