Z3 randomly ignores timeout parameter

[SeeSpring]

When the following code is run

#include <z3.h>

int main(int argc, char const *argv[]) {
    Z3_config cfg = Z3_mk_config();
    Z3_set_param_value(cfg, "timeout", "1");
    Z3_context ctx = Z3_mk_context_rc(cfg);
    Z3_set_error_handler(ctx, NULL);

    Z3_sort int_sort = Z3_mk_int_sort(ctx);

    Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), int_sort);
    Z3_inc_ref(ctx, x);
    Z3_ast y = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "y"), int_sort);
    Z3_inc_ref(ctx, y);
    Z3_ast z = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "z"), int_sort);
    Z3_inc_ref(ctx, z);

    Z3_ast x_cube = Z3_mk_mul(ctx, 3, (Z3_ast[3]){x, x, x});
    Z3_inc_ref(ctx, x_cube);
    Z3_ast y_cube = Z3_mk_mul(ctx, 3, (Z3_ast[3]){y, y, y});
    Z3_inc_ref(ctx, y_cube);
    Z3_ast z_cube = Z3_mk_mul(ctx, 3, (Z3_ast[3]){z, z, z});
    Z3_inc_ref(ctx, z_cube);

    Z3_ast sum_of_cubes = Z3_mk_add(ctx, 3, (Z3_ast[3]){x_cube, y_cube, z_cube});
    Z3_inc_ref(ctx, sum_of_cubes);
    Z3_ast i_42 = Z3_mk_int64(ctx, 42, int_sort);
    Z3_inc_ref(ctx, i_42);
    Z3_ast sum_of_cubes_is_42 = Z3_mk_eq(ctx, sum_of_cubes, i_42);
    Z3_inc_ref(ctx, sum_of_cubes_is_42);

    Z3_solver solver = Z3_mk_solver(ctx);
    Z3_solver_inc_ref(ctx, solver);
    Z3_solver_assert(ctx, solver, sum_of_cubes_is_42);

    Z3_lbool result = Z3_solver_check(ctx, solver);

    printf("%i\n", result);

    Z3_solver_dec_ref(ctx, solver);

    Z3_dec_ref(ctx, z_cube);
    Z3_dec_ref(ctx, y_cube);
    Z3_dec_ref(ctx, x_cube);

    Z3_dec_ref(ctx, z);
    Z3_dec_ref(ctx, y);
    Z3_dec_ref(ctx, x);

    Z3_dec_ref(ctx, Z3_sort_to_ast(ctx, int_sort));

    Z3_dec_ref(ctx, sum_of_cubes_is_42);
    Z3_dec_ref(ctx, i_42);
    Z3_dec_ref(ctx, sum_of_cubes);

    Z3_del_context(ctx);
    Z3_del_config(cfg);

    return 0;
}

(Derived from this test in the Rust package)

the program usually hangs despite the 1m timeout. Some runs will quickly return 0

[NikolajBjorner]

@nunoplopes - stack trace suggests race condition around scoped-timer. It is waiting for a lock inside a tactic.
This pull request #5371 addresses race conditions and requires attention.

[NikolajBjorner]

This seems fixed now, thanks @zhouzhenghui; and @nunoplopes for merging the pull request.

[rindPHI]

I encountered this issue again: Solver does not terminate despite a set timeout. I reduced it as much as I could:

import z3


def make_formula(number: int, should_terminate: bool) -> z3.BoolRef:
    formula = f"""
    (assert (forall 
      ((container String) (number String))
      (=> (and 
            (str.contains start container) 
            (str.contains container number) 
            {'(= (str.++ number (str.++ " * " "<number>")) container)' if not should_terminate else ''})
          (exists 
            ((elem String))
            (and 
              (str.contains number elem)
              (<= (if (= (str.at elem 0) "-") 
                    (* -1 (str.to.int (str.substr elem 1 (- (str.len elem) 1))))
                    (str.to.int elem))
                  {number}))))))"""

    start = z3.String("start")
    return z3.parse_smt2_string(formula, decls={"start": start})[0]


# Terminates
formula = z3.Not(z3.Implies(make_formula(-100, True), make_formula(-50, True)))

s = z3.Solver()
s.set("timeout", 100)
s.append(formula)
print(s.check())

# Diverges
formula = z3.Not(z3.Implies(make_formula(-100, False), make_formula(-50, False)))

s = z3.Solver()
s.set("timeout", 100)
s.append(formula)
print(s.check())

As you see, you can make the solver terminate / diverge by not adding / adding a specific premise to the formulas for which I check the implication. I would understand an "unknown" result, but nontermination despite the timeout is not the best possible outcome ;)

I'm using Z3 4.8.14.0.

[nunoplopes]

Please file a new bug report. Your bug is unrelated with the timeout mechanism.
This is the QI or the seq_rewriter that get stuck without checking for resource limits. See the trace:

#1  0x00007ffff6a7c57a in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) [clone .constprop.0] ()
#2  0x00007ffff6a824fe in ast_manager::mk_app(int, int, expr*, expr*) ()
#3  0x00007ffff667e408 in seq_rewriter::mk_str_stoi(expr*, obj_ref<expr, ast_manager>&) ()
#4  0x00007ffff669483b in seq_rewriter::mk_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&)
#5  0x00007ffff6645b54 in (anonymous namespace)::th_rewriter_cfg::reduce_app(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ()
#6  0x00007ffff664965b in rewriter_tpl<(anonymous namespace)::th_rewriter_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ()
#7  0x00007ffff5e5fdc2 in smt::qi_queue::instantiate(smt::qi_queue::entry&) ()
#8  0x00007ffff5e60932 in smt::qi_queue::instantiate() ()
#9  0x00007ffff5f4cac1 in smt::context::propagate() ()
#10 0x00007ffff5f52938 in smt::context::init_assumptions(ref_vector<expr, ast_manager> const&) ()