Am I using z3 :timeout correctly with C++ interface for Linux?

Question

I'm trying to get the z3 solver to timeout after 0.1s on this example (factoring a 32-bit product of two primes), using the C++ interface. It works on Windows (VC++ 2013), but not on Linux (CentOS 6.5), where the solver runs to completion in around 2.5s (debug build). This post indicates that the command-line timeout was only supported on Windows back in 2012 with z3 v3.2, but this was supposed to be fixed in the next release - we're using z3 v4.4, according to the RELEASE_NOTES. Am I using the timeout functionality correctly for the C++ interface, or is this not supported on Linux?

(Note: this code sample uses the concat definition from here. The TEST, EXPECT_EQ, and EXPECT_TRUE macros are gtest testing macros, that should be self-explanatory.)

    TEST(Z3Basic, Factorize32BitWithTimeout) {
    try {
        context c;
        solver s(c);

        expr x = c.bv_const("x", 16);
        expr y = c.bv_const("y", 16);
        expr prod = c.bv_val(0xc4f7d27bll, 32);

        expr pad = c.bv_val(0, 16);

        params p(c);
        p.set(":timeout", 100u);
        s.set(p);
        expr conjecture = prod == concat(pad, x) * concat(pad, y);
        s.add(conjecture);
        check_result r = s.check();
        EXPECT_EQ(unknown, r);
        if (r == sat)
            std::cout << s.get_model() << "\n";
    }
    catch (exception ex) {
        EXPECT_TRUE(false) << "Exception thrown: " << ex << "\n";
    }

}

On Windows debug, this runs the whole test in around 210ms, and passes with an unknown return code. On Linux, it runs to completion and fails:

[ RUN      ] Z3Basic.Factorize32BitWithTimeout
/home/dave_local/Projects/trunk/CoreApp/z3Interface/UnitTests/TestZ3.cpp:492: Failure
Value of: r
  Actual: sat
Expected: unknown
(define-fun y () (_ BitVec 16)
  #xd279)
(define-fun x () (_ BitVec 16)
  #xef93)
[  FAILED  ] Z3Basic.Factorize32BitWithTimeout (2565 ms)

Any suggestions/information?

Answer 1

Timeout through the API is definitely supported. Maybe 100ms on your Linux box is too much? Can you try with a smaller timeout?

If it still fails, could you file a bug report with a short, self-contained, reproducing test case? Thanks!