{"action":"reopened","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/307","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/307/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/307/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/307/events","html_url":"https://github.com/Z3Prover/z3/issues/307","id":116503425,"number":307,"title":"C API : \"timeout\" seems not to work in the latest unstable-branch","user":{"login":"martin2011","id":5909877,"avatar_url":"https://avatars.githubusercontent.com/u/5909877?v=3","gravatar_id":"","url":"https://api.github.com/users/martin2011","html_url":"https://github.com/martin2011","followers_url":"https://api.github.com/users/martin2011/followers","following_url":"https://api.github.com/users/martin2011/following{/other_user}","gists_url":"https://api.github.com/users/martin2011/gists{/gist_id}","starred_url":"https://api.github.com/users/martin2011/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/martin2011/subscriptions","organizations_url":"https://api.github.com/users/martin2011/orgs","repos_url":"https://api.github.com/users/martin2011/repos","events_url":"https://api.github.com/users/martin2011/events{/privacy}","received_events_url":"https://api.github.com/users/martin2011/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":8,"created_at":"2015-11-12T08:41:50Z","updated_at":"2015-11-14T17:51:15Z","closed_at":null,"body":"I get the source codes of unstable-branch from : https://github.com/Z3Prover/z3/tree/unstable-backup\r\nIn 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)\r\nTimeout is set  with 1 milliseconds  by:\r\n\r\n    `Z3_set_param_value(cfg, \"timeout\", \"1u\");`\r\n\r\nthen 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()`.\r\n\r\nThe following code list is a triggered example  with gcc-4.8 under ubuntu-12.04-64\r\n```\r\n    Z3_config cfg=Z3_mk_config();\r\n\tZ3_set_param_value(cfg, \"timeout\", \"1u\");\r\n\tZ3_context ctx=Z3_mk_context(cfg);\r\n\tZ3_sort float_sort, long_sort, double_sort;\r\n\tZ3_ast roundingmode=Z3_mk_fpa_round_nearest_ties_to_even(ctx);\r\n\tfloat_sort=Z3_mk_fpa_sort_32(ctx);\r\n\tdouble_sort=Z3_mk_fpa_sort_64(ctx);\r\n\tlong_sort=Z3_mk_bv_sort(ctx,64);\r\n\tZ3_ast b=Z3_mk_const(ctx,Z3_mk_string_symbol(ctx,\"b\"),long_sort);\r\n\tZ3_ast castb=Z3_mk_fpa_to_fp_signed(ctx,roundingmode,b,float_sort);\r\n\tZ3_ast a=Z3_mk_const(ctx,Z3_mk_string_symbol(ctx,\"a\"),float_sort);\r\n\tZ3_ast aaddcastb=Z3_mk_fpa_add(ctx,roundingmode,castb,a);\r\n\tZ3_ast castaaddcastb=Z3_mk_fpa_to_fp_float(ctx,roundingmode,aaddcastb,double_sort);\r\n\r\n\tZ3_ast c=Z3_mk_const(ctx,Z3_mk_string_symbol(ctx,\"c\"),double_sort);\r\n\tZ3_ast caddcastadcastb=Z3_mk_fpa_add(ctx,roundingmode,c,castaaddcastb);\r\n\r\n\tZ3_ast castcadd=Z3_mk_fpa_to_fp_float(ctx,roundingmode,caddcastadcastb,float_sort);\r\n\r\n\tZ3_ast iszero=Z3_mk_fpa_is_zero(ctx,castcadd);\r\n\tZ3_assert_cnstr(ctx,iszero);\r\n\tZ3_model m=0;\r\n\tstd::clock_t begin_time= std::clock();\r\n\tZ3_lbool res=Z3_check_and_get_model(ctx,&m);\r\n\tstd::cout << float( clock () - begin_time ) /  CLOCKS_PER_SEC;\r\n\tstd::cout<<std::endl;\r\n\tif (res==Z3_L_TRUE)\r\n\t{\r\n\t\tstd::cout<<\"sat!\\n\";\t\t\r\n\t\tstd::cout<<Z3_model_to_string(ctx,m)<<std::endl;;\r\n\t}else if (res==Z3_L_FALSE)\r\n\t{\r\n\t\tstd::cout<<\"unsat!\\n\";\r\n\t} \r\n\telse\r\n\t{\r\n\t\tstd::cout<<\"unknown!\\n\";\r\n\t}\r\n```"}}