C API : "timeout" seems not to work in the latest unstable-branch

[martin2011]

I get the source codes of unstable-branch from : https://github.com/Z3Prover/z3/tree/unstable-backup In my project, I use pure C API. I use Z3_assert_cnstr() to add a constraint, and Z3_check_and_get_model() to check result. (I asked another related question in StackOverflow :http://stackoverflow.com/questions/33624606/unknown-parameter-timeout-in-z3-set-param-valuecfg-timeout-10) Timeout is set with 1 milliseconds by:

`Z3_set_param_value(cfg, "timeout", "1u");`

then I add several constraints (seems failure with "1u" millisecond) and expect an unknown result, however, it gets a sat result with 81.75 seconds, which is got from counting the time difference between before Z3_check_and_get_model() and after Z3_check_and_get_model().

The following code list is a triggered example with gcc-4.8 under ubuntu-12.04-64

    Z3_config cfg=Z3_mk_config();
    Z3_set_param_value(cfg, "timeout", "1u");
    Z3_context ctx=Z3_mk_context(cfg);
    Z3_sort float_sort, long_sort, double_sort;
    Z3_ast roundingmode=Z3_mk_fpa_round_nearest_ties_to_even(ctx);
    float_sort=Z3_mk_fpa_sort_32(ctx);
    double_sort=Z3_mk_fpa_sort_64(ctx);
    long_sort=Z3_mk_bv_sort(ctx,64);
    Z3_ast b=Z3_mk_const(ctx,Z3_mk_string_symbol(ctx,"b"),long_sort);
    Z3_ast castb=Z3_mk_fpa_to_fp_signed(ctx,roundingmode,b,float_sort);
    Z3_ast a=Z3_mk_const(ctx,Z3_mk_string_symbol(ctx,"a"),float_sort);
    Z3_ast aaddcastb=Z3_mk_fpa_add(ctx,roundingmode,castb,a);
    Z3_ast castaaddcastb=Z3_mk_fpa_to_fp_float(ctx,roundingmode,aaddcastb,double_sort);

    Z3_ast c=Z3_mk_const(ctx,Z3_mk_string_symbol(ctx,"c"),double_sort);
    Z3_ast caddcastadcastb=Z3_mk_fpa_add(ctx,roundingmode,c,castaaddcastb);

    Z3_ast castcadd=Z3_mk_fpa_to_fp_float(ctx,roundingmode,caddcastadcastb,float_sort);

    Z3_ast iszero=Z3_mk_fpa_is_zero(ctx,castcadd);
    Z3_assert_cnstr(ctx,iszero);
    Z3_model m=0;
    std::clock_t begin_time= std::clock();
    Z3_lbool res=Z3_check_and_get_model(ctx,&m);
    std::cout << float( clock () - begin_time ) /  CLOCKS_PER_SEC;
    std::cout<<std::endl;
    if (res==Z3_L_TRUE)
    {
        std::cout<<"sat!\n";        
        std::cout<<Z3_model_to_string(ctx,m)<<std::endl;;
    }else if (res==Z3_L_FALSE)
    {
        std::cout<<"unsat!\n";
    } 
    else
    {
        std::cout<<"unknown!\n";
    }

[wintersteiger]

The unstable branch has been removed and you are using an old backup of it (unstable-backup). All new development goes directly into the master branch, so please switch over to that and see whether the same problem still exists there.

[martin2011]

Yes, it still exists. However, the example above is unfit for testing because that example will trigger an "Assertion Violation" exception. In the following, an example for triggering "timeout" does not work is listed:

     Z3_config cfg=Z3_mk_config();
    Z3_set_param_value(cfg, "timeout", "1u");
    Z3_context ctx=Z3_mk_context(cfg);
    Z3_sort float_sort,bv_sort;
    float_sort=Z3_mk_fpa_sort_32(ctx);
    bv_sort=Z3_mk_bv_sort(ctx,32);
    Z3_ast x=Z3_mk_const(ctx,Z3_mk_string_symbol(ctx,"x"),bv_sort);
    Z3_ast a=Z3_mk_const(ctx,Z3_mk_string_symbol(ctx,"a"),bv_sort);
    Z3_ast a2=Z3_mk_bvmul(ctx,a,a);
    Z3_ast x2=Z3_mk_bvmul(ctx,x,x);
    Z3_ast bvfive=Z3_mk_numeral(ctx,"5",bv_sort);
    Z3_ast a25=Z3_mk_bvadd(ctx,a2,bvfive);

    Z3_ast x2gta25=Z3_mk_bvsgt(ctx,x2,a25);
    Z3_assert_cnstr(ctx,x2gta25);

    Z3_ast y=Z3_mk_const(ctx,Z3_mk_string_symbol(ctx,"y"),float_sort);
    Z3_ast b=Z3_mk_const(ctx,Z3_mk_string_symbol(ctx,"b"),float_sort);
    Z3_ast roundtonearest_even=Z3_mk_fpa_round_nearest_ties_to_even(ctx);
    Z3_ast b2=Z3_mk_fpa_mul(ctx,roundtonearest_even,b,b);

    Z3_ast b2b=Z3_mk_fpa_add(ctx,roundtonearest_even,b2,b);
    Z3_ast ffive=Z3_mk_fpa_numeral_float(ctx,5.0f,float_sort);
    Z3_ast b2bf=Z3_mk_fpa_add(ctx,roundtonearest_even,b2b,ffive);
    Z3_ast y2=Z3_mk_fpa_mul(ctx,roundtonearest_even,y,y);
    Z3_ast y2ltb2bf=Z3_mk_fpa_gt(ctx,y2,b2bf);
    Z3_assert_cnstr(ctx,y2ltb2bf);
    Z3_model m=0;
    std::clock_t begin_time= std::clock();
    Z3_lbool res=Z3_check_and_get_model(ctx,&m);
    std::cout << float( clock () - begin_time ) /  CLOCKS_PER_SEC;
    std::cout<<"\n";
    if (res==Z3_L_TRUE)
    {
        std::cout<<"sat!"<<std::endl;
        std::cout<<m<<std::endl;
        std::cout<<Z3_model_to_string(ctx,m)<<std::endl;
    }else if (res==Z3_L_FALSE)
    {
        std::cout<<"unsat!"<<std::endl;
    } 
    else
    {
        std::cout<<"unknown!"<<std::endl;
    }

The example listed at the beginning will trigger an "ASSERTION VIOLATION" exception, the output of running is as:

ASSERTION VIOLATION
File: ../src/ast/fpa/fpa2bv_converter.cpp
Line: 2655
m_bv_util.is_bv(args[0])
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

In summary, in this issue, there are two "bug " reports.

1) Th first is timeout does not work, which can be triggered by the example in this comment.

2) The second is "Assertion Violation" exception, which happened in the example listed in the example at the main body. Both of these "bugs" are happened in the latest master branch.

I use the "ASSERTION VIOLATION" exception example at the beginning due to I use the unstable-branch in the first experiment and there is not "Assertion violation " in that version( which is mentioned in my question at StackOverflow).

Is it necessary to open another new issue to describe the "Assertion Violation" exception?

[wintersteiger]

Thanks for the report! We won't need a separate issue for the assertion failure, that was just an out of date assertion which shouldn't be reported anymore.

[wintersteiger]

Note that Z3_check_and_get_model is deprecated, so should not be used in new code anymore. Our C-examples haven't been updated yet, but you can see how the new solver interface works in our C++ examples, e.g., the DeMorgan example.

I've committed a fix for this particular problem with timeouts. @NikolajBjorner could you take a look at this to check whether my change could break other things like the rlimit handling?

[NikolajBjorner]

Change is perfectly fine. The use of the C API in the repro above is potentially very unsafe: the caller does not take a reference count on the objects (AST pointers) returned from Z3. Their life-time is undefined if they are not used immediately after to define a new AST of if a reference count is not acquired. The C++ wrappers handle this automatically so it is much better to use the C++ mode.

[martin2011]

@NikolajBjorner, is that meaning a Z3_ast made from Z3_mk_const is not copied in current ctx, and it's lifetime will be ended and cannot be used any more out of this function? (I am unfamiliar with the inner architecture of Z3 though I have a try to understand)

Besides, is it safe to use Z3_solver_assert() to add a constraint, and check by Z3_solver_check() ? Pure C++ API is not an easy way for me to use floating-point theory ?

At last, could you inform me when you fix the "timeout" issue?. I test this morning, it still exists.

[wintersteiger]

Yes, when using the C API, you are responsible for reference counting. Every time you get a Z3_ast (or most other Z3 objects types), you wall have to call inc_ref and every time you remove a reference to a Z3_ast you have to call dec_ref by yourself. Like Nikolaj said, this is not necessary in the C++ API if you use `expr' objects, which do the reference counting for you, even when used in combination with pure C functions; see the C++ example to get started with that.

Z3_solver_assert(...) is the right function to add constraints to a solver, so they can be checked by using Z3_solver_check(). See C++ example again.

The timeout issue is fixed. Please get a fresh copy of the master branch and compile it from scratch. I think "1u" is not a valid timeout value and I will add checks for invalid strings. Try testing this issue by setting the timeout to "1000" and then to "2000" to see whether the fix works in your setting.

[wintersteiger]

As I said before, Z3_check_and_get_model is deprecated and should not be used anymore; everything in this example seems OK to me when solvers are used.

The old Z3_check_and_get_model now also understands the timeout correctly, but the (smt.simplifier ...) takes around 2 seconds during which it is uninterruptable, so it may look like it doesn't respect very small timeouts. This is likely caused by the floating-point theory rewriter which is also used in the newer solvers, so there is probably a way to trigger the same problem via other routes, so I'm re-opening this issue.

[wintersteiger]

Actually, this is only true in debug mode. In release mode the simplifier takes around 0.21 seconds, so that's also the minimum timeout. Do you have a specific need for very small timeouts? Since this is all deprecated I don't see a reason to invest much time on this. Using solvers everything works fine (it takes .001 seconds), that is with proper reference counting and replacement of Z3_check_and_get_model with

solver s(ctx);
s.add(iszero);
check_result res=s.check();

[martin2011]

Thanks @wintersteiger .

Do you have a specific need for very small timeouts?

No, this is just an example to display. In fact, the timeout maybe set with 1 minute, even ten minutes for floating-point theory.

this is only true in debug mode

Yes, all of these are happened in debug mode. And all the configurations other than timeout are default.

Like Nikolaj said, this is not necessary in the C++ API if you use `expr' objects, which do the reference counting for you, even when used in combination with pure C functions; see the C++ example to get started with that.

I have used C++ API before with real theory, and I start to use C API for applying floating-point theory. I had a try to use expr at the beginning, however, there were various kinds of Assertions, exceptions or segment triggered. In using C++ API mode, the working flow of calling a function is: c++ API----> c API -----> back to c++ API, these conversions back and forth maybe to some extent bring in some inconsistent issues with personal specification with each level API and trigger the Assertions or segment, thus, I try to use C function directly. On the other hand, my misusing of the API may also be major reason for these happened. In the following, I try to find a reasonable way to using c or c++ API in my project, Thanks again.

[martin2011]

The timeout issue is fixed

yes, it is true for testing with the fresh code.