mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity
5564 commits 23 branches 48 tags 157 MiB
Commit graph

5564 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger 2bbca192e3 member init order 2016-05-20 20:16:45 +01:00
Christoph M. Wintersteiger 4ed2b8a0f9 Bugfix for unspecified FP model values. 2016-05-20 20:15:08 +01:00
Christoph M. Wintersteiger cae53c3ec2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-20 19:55:01 +01:00
Christoph M. Wintersteiger 1cc8146aba Bugfixes for FP UFs and arrays. 2016-05-20 19:53:57 +01:00
Christoph M. Wintersteiger 80731ef364 Exposed OP_FPA_MIN/MAX_I to the API 2016-05-20 19:40:45 +01:00
Nikolaj Bjorner d12efb6097 remove min/max, use qmax; disable cancellation during model evaluation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-19 13:10:43 -07:00
Nikolaj Bjorner 1aa3fdab8a remove min/max, use qmax; disable cancellation during model evaluation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-19 13:04:20 -07:00
Nikolaj Bjorner d2622da747 fix unused-but-set-variable warnings reported in #579 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-18 11:03:31 -07:00
Nikolaj Bjorner 3a6e6df4f5 fix unused-but-set-variable warnings reported in #579 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-18 11:02:10 -07:00
Nikolaj Bjorner 9aaee8616a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-18 09:58:50 -07:00
Nikolaj Bjorner 85be486c1e add ite reduction to canonizer, remove it from ad-hoc routine 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-18 09:58:34 -07:00
Nikolaj Bjorner 5e7db2e3e2 disable mk_array_eq as it breaks model evaluation/validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-18 08:29:24 -07:00
Christoph M. Wintersteiger 71a03dbeb3 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-18 09:58:11 +01:00
Nikolaj Bjorner cc3bfe8da2 removing warnings for unused variables, #579 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-17 16:02:08 -07:00
Nikolaj Bjorner 09b8c0e7fa removing warnings for unused variables, #579 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-17 15:59:06 -07:00
Nikolaj Bjorner 40f8e16273 removing warnings for unused variables, #579 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-17 14:00:30 -07:00
Nikolaj Bjorner 96e157e201 fix warnings for unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-17 13:54:22 -07:00
Christoph M. Wintersteiger df81ab72f5 Bug and performance fixes for FP UFs. 2016-05-17 16:35:45 +01:00
Nikolaj Bjorner ec565ae7a0 fixes to #596 and #592: use exponential step increments on integer problems, align int.to.str with canonizer and disequality checker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-17 01:00:42 -07:00
Nikolaj Bjorner 5250c3b9ed ensure reference ownership on frame elements to avoid crashes due to nnf. Issue #588 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-16 09:37:15 -07:00
Nikolaj Bjorner 6f5785338a add line/pos information for pattern warnings. Issue #607 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-16 08:59:58 -07:00
Nikolaj Bjorner 69ccc02931 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-16 08:35:12 -07:00
Nikolaj Bjorner f1b63691d8 Fixing issue #605 rlimit responsiveness in mam 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-16 08:35:04 -07:00
Christoph M. Wintersteiger 89598e0141 Merge pull request #608 from wintersteiger/fprti-rna-fix 
Fix for #586, RNA rounding for fp.roundToIntegral.
 2016-05-16 16:21:35 +01:00
Christoph M. Wintersteiger 85366f247f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-16 16:17:18 +01:00
Christoph M. Wintersteiger 99f5269b78 debug output fix 2016-05-16 16:15:44 +01:00
Nikolaj Bjorner 121f79b198 Merge pull request #603 from manueljacob/master 
Expose Z3_mk_bv2int's is_signed parameter in Python API.
 2016-05-16 07:56:37 -07:00
Nikolaj Bjorner beda356e32 Merge pull request #606 from teodorvlasov/master 
add DOTNET_ENABLED to globals in parser_options of mk_*_dist
 2016-05-16 07:56:10 -07:00
Nikolaj Bjorner a8fca8f77e remove unused private fields 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-15 20:28:46 -07:00
Nikolaj Bjorner cd937c07f3 return proper ast-option from get_const_interp function insetad of raising exceptions from inside the C API. Fixes discrepancy with documentation and behavior across extensions of the API. Issue #587 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-15 13:29:38 -07:00
Nikolaj Bjorner e5ca676251 initialize manager to avoid unrelated error message, issue #604 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-15 12:59:42 -07:00
Nikolaj Bjorner 7fb30c38ae disallow illegal use per #604 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-15 12:49:07 -07:00
Teodor Vlasov 886759a58c add DOTNET_ENABLED in parser_options of mk_*_dist 2016-05-15 22:36:12 +03:00
Nikolaj Bjorner 10cdd527ca strengthening length properties for int.to.str. Issue #589 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-15 12:27:04 -07:00
Nikolaj Bjorner 99314b7252 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-15 11:34:55 -07:00
Nikolaj Bjorner 42726171b5 add limit checks in Grobner. Issue #599 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-15 11:34:48 -07:00
Christoph M. Wintersteiger 44b0a6ddbc Tentative fix for #586. 2016-05-14 18:42:10 +01:00
Christoph M. Wintersteiger bb2c5972c7 Bugfixes for UFs in theory_fpa. 
Fixes #591, but performance issues remain.
 2016-05-14 18:21:53 +01:00
Christoph M. Wintersteiger c87ffbc3a5 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-14 14:29:21 +01:00
Christoph M. Wintersteiger 3fde81aea6 Style 2016-05-14 14:29:13 +01:00
Manuel Jacob 7e3dfb4617 Expose Z3_mk_bv2int's is_signed parameter in Python API. 2016-05-13 23:17:05 +02:00
Christoph M. Wintersteiger b0bd848a27 Merge pull request #597 from nunoplopes/master 
change Z3_get_decl_kind API to correctly identify OP_B*_I and OP_B*_NO_OVFL instead of returning Z3_OP_UNINTERPRETED
 2016-05-12 18:36:14 +01:00
Christoph M. Wintersteiger 0ddf2d92fe removed unused variables 2016-05-12 15:20:50 +01:00
Christoph M. Wintersteiger 4ca09e9e9a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-12 15:13:36 +01:00
Christoph M. Wintersteiger 12a8d0d02b mpf debug cleanup 2016-05-12 15:12:46 +01:00
Christoph M. Wintersteiger 37f4cc89c9 Merge pull request #600 from wintersteiger/new-mpf-rem 
New mpf_manager::rem
 2016-05-12 14:16:53 +01:00
Christoph M. Wintersteiger dd83495d5d New implementation of mpf_manager::rem. 
Partially addresses #561
 2016-05-12 14:15:24 +01:00
Christoph M. Wintersteiger ed1861d90d Merge branch 'master' of https://github.com/Z3Prover/z3 into new-mpf-rem 2016-05-12 13:30:16 +01:00
Nuno Lopes d4f3ea99da Merge pull request #598 from seahorn/model_evaluator_array_fix 
bug fix in model_evaluator for array equality
 2016-05-12 08:33:27 +01:00
Arie Gurfinkel d1f8b06ec4 bug fix in model_evaluator for array equality 2016-05-11 22:44:11 -04:00