Infinite loop (rlimit leak?) in 4.15.3

[mtzguido]

Hi, the following file:

loop.smt2.txt

is processed rather quickly by Z3 4.15.3:

$ ramon z3-4.15.3 loop.smt2
[...]
Done!
[...]
ramon: walltime             0.643s

(the last query comes back unknown, but that's not a problem)

But, if I increase the rlimit near the bottom of the file by just one unit (to 1285596), the last query diverges. It ran for at least 10 minutes on my machine.

I couldn't repro this in master, but it's again probably a very brittle situation. Changing the random seed also avoids it.

[NikolajBjorner]

If there is a code-path where rlimit isnt being checked, then for your version of the binaries, run it in a debugger and when it hangs, break. The stack will say where execution resides without checks.
It is then possible to correlate master with this code path to check if it has been addressed or not.

[mtzguido]

Here's a stack trace, and then I used finish to run each frame until completion. It seems to get stuck in nlsat::solver::imp::search_check(). Looking at it, there's a while(true) loop without any checkpoint in it, so maybe that's the culprit?

^C
Program received signal SIGINT, Interrupt.
0x0000555556e22f68 in u_gcd(unsigned int, unsigned int) [clone .part.0] ()
(gdb) where
#0  0x0000555556e22f68 in u_gcd(unsigned int, unsigned int) [clone .part.0] ()
#1  0x0000555556e322c6 in mpz_manager<false>::gcd(mpz const&, mpz const&, mpz&) ()
#2  0x0000555556e32c50 in mpz_manager<false>::gcd(unsigned int, mpz const*, mpz&) ()
#3  0x0000555556d72cbd in upolynomial::core_manager::get_primitive_and_content(unsigned int, mpz const*, svector<mpz, unsigned int>&, mpz&) ()
#4  0x0000555556d72e8b in upolynomial::core_manager::mod_gcd(unsigned int, mpz const*, unsigned int, mpz const*, svector<mpz, unsigned int>&) ()
#5  0x0000555556d7814a in upolynomial::manager::factor_core(unsigned int, mpz const*, upolynomial::core_manager::factors&, polynomial::factor_params const&) ()
#6  0x0000555556d66275 in algebraic_numbers::manager::imp::isolate_roots(upolynomial::scoped_numeral_vector const&, svector<algebraic_numbers::anum, unsigned int>&) ()
#7  0x0000555556d571ec in algebraic_numbers::manager::imp::isolate_roots(obj_ref<polynomial::polynomial, polynomial::manager> const&, polynomial::var2value<algebraic_numbers::manager, algebraic_numbers::anum> const&, svector<algebraic_numbers::anum, unsigned int>&, bool) [clone .isra.0] ()
#8  0x0000555556742934 in nlsat::evaluator::eval(nlsat::atom*, bool) ()
#9  0x000055555670bf5e in nlsat::solver::imp::search() [clone .constprop.0] ()
#10 0x000055555670e3b1 in nlsat::solver::imp::search_check() [clone .constprop.0] ()
#11 0x000055555670a91f in nlsat::solver::imp::check() [clone .constprop.0] ()
#12 0x0000555556616aba in nra::solver::imp::check() ()
#13 0x000055555667d135 in nla::core::check() ()
#14 0x0000555555e9645c in smt::theory_lra::imp::final_check_eh() ()
#15 0x000055555602adbf in smt::context::final_check() ()
#16 0x000055555602b4a5 in smt::context::bounded_search() ()
#17 0x000055555602c4c0 in smt::context::search() ()
#18 0x000055555602c938 in smt::context::check(unsigned int, expr* const*, bool) ()
#19 0x0000555556404229 in solver_na2as::check_sat_core(unsigned int, expr* const*) ()
#20 0x0000555556431182 in solver::check_sat(unsigned int, expr* const*) ()
#21 0x00005555563d0cf5 in cmd_context::check_sat(unsigned int, expr* const*) ()
#22 0x00005555563b53bd in smt2::parser::operator()() ()
#23 0x000055555639cf95 in parse_smt2_commands(cmd_context&, std::basic_istream<char, std::char_traits<char> >&, bool, params_ref const&, char const*)
    ()
#24 0x00005555557d9e3e in read_smtlib2_commands(char const*) ()
#25 0x00005555557c44ae in main ()
(gdb) finish
Run till exit from #0  0x0000555556e22f68 in u_gcd(unsigned int, unsigned int) [clone .part.0] ()
0x0000555556e322c6 in mpz_manager<false>::gcd(mpz const&, mpz const&, mpz&) ()
(gdb)
Run till exit from #0  0x0000555556e322c6 in mpz_manager<false>::gcd(mpz const&, mpz const&, mpz&) ()
0x0000555556e32c50 in mpz_manager<false>::gcd(unsigned int, mpz const*, mpz&) ()
(gdb)
Run till exit from #0  0x0000555556e32c50 in mpz_manager<false>::gcd(unsigned int, mpz const*, mpz&) ()
0x0000555556d72cbd in upolynomial::core_manager::get_primitive_and_content(unsigned int, mpz const*, svector<mpz, unsigned int>&, mpz&) ()
(gdb)
Run till exit from #0  0x0000555556d72cbd in upolynomial::core_manager::get_primitive_and_content(unsigned int, mpz const*, svector<mpz, unsigned int>&, mpz&) ()
0x0000555556d72e8b in upolynomial::core_manager::mod_gcd(unsigned int, mpz const*, unsigned int, mpz const*, svector<mpz, unsigned int>&) ()
(gdb)
Run till exit from #0  0x0000555556d72e8b in upolynomial::core_manager::mod_gcd(unsigned int, mpz const*, unsigned int, mpz const*, svector<mpz, unsigned int>&) ()
0x0000555556d7814a in upolynomial::manager::factor_core(unsigned int, mpz const*, upolynomial::core_manager::factors&, polynomial::factor_params const&) ()
(gdb)
Run till exit from #0  0x0000555556d7814a in upolynomial::manager::factor_core(unsigned int, mpz const*, upolynomial::core_manager::factors&, polynomial::factor_params const&) ()
0x0000555556d66275 in algebraic_numbers::manager::imp::isolate_roots(upolynomial::scoped_numeral_vector const&, svector<algebraic_numbers::anum, unsigned int>&) ()
(gdb)
Run till exit from #0  0x0000555556d66275 in algebraic_numbers::manager::imp::isolate_roots(upolynomial::scoped_numeral_vector const&, svector<algebraic_numbers::anum, unsigned int>&) ()
0x0000555556d571ec in algebraic_numbers::manager::imp::isolate_roots(obj_ref<polynomial::polynomial, polynomial::manager> const&, polynomial::var2value<algebraic_numbers::manager, algebraic_numbers::anum> const&, svector<algebraic_numbers::anum, unsigned int>&, bool) [clone .isra.0] ()
(gdb)
Run till exit from #0  0x0000555556d571ec in algebraic_numbers::manager::imp::isolate_roots(obj_ref<polynomial::polynomial, polynomial::manager> const&, polynomial::var2value<algebraic_numbers::manager, algebraic_numbers::anum> const&, svector<algebraic_numbers::anum, unsigned int>&, bool) [clone .isra.0] ()
0x0000555556742934 in nlsat::evaluator::eval(nlsat::atom*, bool) ()
(gdb)
Run till exit from #0  0x0000555556742934 in nlsat::evaluator::eval(nlsat::atom*, bool) ()
0x000055555670bf5e in nlsat::solver::imp::search() [clone .constprop.0] ()
(gdb)
Run till exit from #0  0x000055555670bf5e in nlsat::solver::imp::search() [clone .constprop.0] ()
0x000055555670e3b1 in nlsat::solver::imp::search_check() [clone .constprop.0] ()
(gdb)
Run till exit from #0  0x000055555670e3b1 in nlsat::solver::imp::search_check() [clone .constprop.0] ()
^C
Program received signal SIGINT, Interrupt.

[mtzguido]

Z3 master also loops here with random seed = 11, but adding checkpoint() calls there did not seem to help, so maybe I'm misunderstanding something.

[mtzguido]

Thanks! That does seem to fix it, at least 5000 random seeds didn't hit it. It seems to have been a more general issue about rlimit tracking?