A strange behavior: Only text replacement causes divergence

[chansey97]

Hi,

I encountered a very strange problem. It might be a z3 bug, but I'm not sure yet (I am a beginner of z3).

The reproduction steps as follows:

1. I have a smtlib file ok.txt which can run normally.

   $ z3 ok.txt > ok-result.txt

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

   Note that there is no _v appeared in ok.txt, so I believe we can do the replacement safely.

   The file before replacement and file after replacement are something like:

   

3. Run the replaced file stuck.txt.

   $ z3 stuck.txt > stuck-result.txt

   Then z3 stuck (seems to diverge when solving nonlinear arithmetic).

The question is that why ok.txt could run normally, but stuck.txt diverged? Is it a bug of z3?

Thanks.

PS. You could replace _v back to _w then it OK again (give you the same file as ok.txt), so I think there is no naming substitution problem.

My test environment:

z3-4.8.12-x64-win on windows 7.

[NikolajBjorner]

You can get the solver to produce solutions by setting the random seed differently on stuck.txt. For example,

 z3 stuck.txt smt.random_seed=1 

Generally this can happen: the solver is trapped in some sequence of bad decisions without escaping. It might be fixable and help with overall performance, but requires investigation to tell.

@levnach - it could be the case that the nla solver uses the same branch and misses some diversity or restart opportunities and therefore gets stuck.

[NikolajBjorner]

A first peek suggests there is a divergence bug. Printing lemmas in nla_core::check we see a sequence:

emmas
lemma:114 ineqs: j86 <= -2223570731460188
(j86 = -371296878 = (j5 = -185648452)*(j81 = 11977319))
[86]    := (-371296878, 0)      [-oo, (-371296878, 0)]
root=j86

expl: (525)j5 <= -185648452
      (526)j81 >= 11977319
(j86 = -371296878 = (j5 = -185648452)*(j81 = 11977319))
[86]    := (-371296878, 0)      [-oo, (-371296878, 0)]
root=j86
[5]    := (-185648452, 0)      [-oo, (-185648452, 0)]
root=j5
[81]    := (11977319, 0)        [(11977319, 0), oo]
root=j81
lemmas
lemma:115 ineqs: j86 <= -13316207984881219329728
(j86 = -2223570731460188 = (j5 = -1111785365730112)*(j81 = 71728088111619))
[86]    := (-2223570731460188, 0)      [-oo, (-2223570731460188, 0)]
root=j86

expl: (532)j5 <= -1111785365730112
      (526)j81 >= 11977319
(j86 = -2223570731460188 = (j5 = -1111785365730112)*(j81 = 71728088111619))
[86]    := (-2223570731460188, 0)      [-oo, (-2223570731460188, 0)]
root=j86
[5]    := (-1111785365730112, 0)      [-oo, (-1111785365730112, 0)]
root=j5
[81]    := (71728088111619, 0)      [(11977319, 0), oo]
root=j81
lemmas
lemma:116 ineqs: j86 <= -2860022501558295871061085257984668473092117
(j86 = -13316207984881219329728 = (j5 = -6658103992440609664882)*(j81 = 429555096286490946121))
[86]    := (-13316207984881219329728, 0)      [-oo, (-13316207984881219329728, 0)]
root=j86

expl: (536)j5 <= -6658103992440609664877
      (539)j81 >= 429555096286490946121
(j86 = -13316207984881219329728 = (j5 = -6658103992440609664882)*(j81 = 429555096286490946121))
[86]    := (-13316207984881219329728, 0)      [-oo, (-13316207984881219329728, 0)]
root=j86
[5]    := (-6658103992440609664882, 0)      [-oo, (-6658103992440609664877, 0)]
root=j5
[81]    := (429555096286490946121, 0)      [(429555096286490946121, 0), oo]
root=j81
lemmas
lemma:117 ineqs: j86 <= -614268620519202242444555128582822858497027262894838236609809912
(j86 = -2860022501558295871061085257984668473092117 = (j5 = -1430011250779147935530542628992334236546072)*(j81 = 92258790372848253905196298644666724938456))
[86]    := (-2860022501558295871061085257984668473092117, 0)      [-oo, (-2860022501558295871061085257984668473092117, 0)]
root=j86

expl: (544)j81 >= 92258790372848253905196298644666724938456
      (536)j5 <= -6658103992440609664877
(j86 = -2860022501558295871061085257984668473092117 = (j5 = -1430011250779147935530542628992334236546072)*(j81 = 92258790372848253905196298644666724938456))
[86]    := (-2860022501558295871061085257984668473092117, 0)      [-oo, (-2860022501558295871061085257984668473092117, 0)]
root=j86
[5]    := (-1430011250779147935530542628992334236546072, 0)      [-oo, (-6658103992440609664877, 0)]
root=j5
[81]    := (92258790372848253905196298644666724938456, 0)      [(92258790372848253905196298644666724938456, 0), oo]
root=j81
lemmas
lemma:118 ineqs: j86 <= -131931108216447943680866681486072532814391534284967300437769138933426533249973747044
(j86 = -614268620519202242444555128582822858497027262894838236609809912 = (j5 = -307134310259601121222277564291411429248513631447419118304904970)*(j81 = 19815116790942007820792100922026543822484750415962523761606772))
[86]    := (-614268620519202242444555128582822858497027262894838236609809912, 0)      [-oo, (-614268620519202242444555128582822858497027262894838236609809912, 0)]
root=j86

expl: (536)j5 <= -6658103992440609664877
      (553)j81 >= 19815116790942007820792100922026543822484750415962523761606772
(j86 = -614268620519202242444555128582822858497027262894838236609809912 = (j5 = -307134310259601121222277564291411429248513631447419118304904970)*(j81 = 19815116790942007820792100922026543822484750415962523761606772))
[86]    := (-614268620519202242444555128582822858497027262894838236609809912, 0)      [-oo, (-614268620519202242444555128582822858497027262894838236609809912, 0)]
root=j86
[5]    := (-307134310259601121222277564291411429248513631447419118304904970, 0)      [-oo, (-6658103992440609664877, 0)]
root=j5
[81]    := (19815116790942007820792100922026543822484750415962523761606772, 0)      [(19815116790942007820792100922026543822484750415962523761606772, 0), oo]
root=j81
lemmas
lemma:119 ineqs: j86 <= -280738988955162872824619220986401716750172107078685317543565229390751351056730192678769266133753484854315613691017937917685387021463971373818322441245144813977780115
(j86 = -131931108216447943680866681486072532814391534284967300437769138933426533249973747044 = (j5 = -65965554108223971840433340743036266407195767142483650218884569466713266624986873536)*(j81 = 4255842200530578828415054241486210735948114009192493562508681901078275266128185389))
[86]    := (-131931108216447943680866681486072532814391534284967300437769138933426533249973747044, 0)      [-oo, (-131931108216447943680866681486072532814391534284967300437769138933426533249973747044, 0)]
root=j86

expl: (562)j81 >= 4255842200530578828415054241486210735948114009192493562508681901078275266128185389
      (559)j5 <= -65965554108223971840433340743036266407195767142483650218884569466713266624986873535
(j86 = -131931108216447943680866681486072532814391534284967300437769138933426533249973747044 = (j5 = -65965554108223971840433340743036266407195767142483650218884569466713266624986873536)*(j81 = 4255842200530578828415054241486210735948114009192493562508681901078275266128185389))
[86]    := (-131931108216447943680866681486072532814391534284967300437769138933426533249973747044, 0)      [-oo, (-131931108216447943680866681486072532814391534284967300437769138933426533249973747044, 0)]
root=j86
[5]    := (-65965554108223971840433340743036266407195767142483650218884569466713266624986873536, 0)      [-oo, (-65965554108223971840433340743036266407195767142483650218884569466713266624986873535, 0)]
root=j5
[81]    := (4255842200530578828415054241486210735948114009192493562508681901078275266128185389, 0)      [(4255842200530578828415054241486210735948114009192493562508681901078275266128185389, 0), oo]
root=j81
lemmas
lemma:120 ineqs: j86 <= -597390418264835112945252424666922193877944192527550247206470880641366707737977530539923989665049658896707924172227733183788357022657352121546483178603058633581686939647517886064208669191092269752810239158200588615661913577704411453871521237810080
(j86 = -280738988955162872824619220986401716750172107078685317543565229390751351056730192678769266133753484854315613691017937917685387021463971373818322441245144813977780115 = (j5 = -140369494477581436412309610493200858375086053539342658771782614695375675528365096339384633066876742427157806845508968958842693510731985686909161220622572406988890071)*(j81 = 9056096417908479768536103902787152153231358292860816694953717077121011324410651376734492455927531769494052054548965739280173774885934560445752336814359510128315488))
[86]    := (-280738988955162872824619220986401716750172107078685317543565229390751351056730192678769266133753484854315613691017937917685387021463971373818322441245144813977780115, 0)      [-oo, (-280738988955162872824619220986401716750172107078685317543565229390751351056730192678769266133753484854315613691017937917685387021463971373818322441245144813977780115, 0)]
root=j86

expl: (566)j81 >= 9056096417908479768536103902787152153231358292860816694953717077121011324410651376734492455927531769494052054548965739280173774885934560445752336814359510128315488
      (559)j5 <= -65965554108223971840433340743036266407195767142483650218884569466713266624986873535
(j86 = -280738988955162872824619220986401716750172107078685317543565229390751351056730192678769266133753484854315613691017937917685387021463971373818322441245144813977780115 = (j5 = -140369494477581436412309610493200858375086053539342658771782614695375675528365096339384633066876742427157806845508968958842693510731985686909161220622572406988890071)*(j81 = 9056096417908479768536103902787152153231358292860816694953717077121011324410651376734492455927531769494052054548965739280173774885934560445752336814359510128315488))
[86]    := (-280738988955162872824619220986401716750172107078685317543565229390751351056730192678769266133753484854315613691017937917685387021463971373818322441245144813977780115, 0)      [-oo, (-280738988955162872824619220986401716750172107078685317543565229390751351056730192678769266133753484854315613691017937917685387021463971373818322441245144813977780115, 0)]
root=j86
[5]    := (-140369494477581436412309610493200858375086053539342658771782614695375675528365096339384633066876742427157806845508968958842693510731985686909161220622572406988890071, 0)      [-oo, (-65965554108223971840433340743036266407195767142483650218884569466713266624986873535, 0)]
root=j5
[81]    := (9056096417908479768536103902787152153231358292860816694953717077121011324410651376734492455927531769494052054548965739280173774885934560445752336814359510128315488, 0)      [(9056096417908479768536103902787152153231358292860816694953717077121011324410651376734492455927531769494052054548965739280173774885934560445752336814359510128315488, 0), oo]
root=j81

It should point to a bug, most likely in bounds propagation,

    if (l_vec.empty() && !done()) 
        m_monomial_bounds();

that produces a succession of bounds with larger numerals.

[chansey97]

@NikolajBjorner Thank you for telling me this information. I set smt.random_seed=1, it works now!

Then I read the random-seed section of smt-lib-reference-v2.6-r2021-05-12.

It says that

:random-seed default: 0 support: optional mode: start

The argument is a numeral for the solver to use as a random seed, in case the solver uses (pseudo-)randomization. The default value of 0 means that the solver can use any random seed—possibly even a different one for each run of the same script. The intended use of the option is to force the solver to produce identical results whenever given identical input (including identical non-zero seeds) on repeated runs of the solver.

Therefore, can I think that this issue is not relevant to the symbol names?

In my current understanding, because the default value of random-seed is 0, so, in fact, z3 defaultly uses a different random seed (e.g. based on the current system time?) every time it starts. The phenomenon about "ok.txt could produces solutions, but stuck.txt stuck" is just an accident. If we are very unfortunate, the ok.txt could get stuck too. Is that right?

Thanks again!