mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity
4227 commits 23 branches 48 tags 157 MiB
Commit graph

4227 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger 4626196907 Eliminated reinterpret_casts. Partially fixes #24, #229. 2015-10-04 15:52:20 +01:00
Christoph M. Wintersteiger c636c87e4d Eliminated unused variable 2015-10-04 15:51:27 +01:00
Christoph M. Wintersteiger 32194b3f36 Eliminated unused variables. 2015-10-04 15:22:10 +01:00
Christoph M. Wintersteiger b20224bc98 Removed or commented unused functions and variables. 2015-10-04 15:21:17 +01:00
Christoph M. Wintersteiger fbac183e32 eliminated unused variable 2015-10-04 15:16:41 +01:00
Christoph M. Wintersteiger 4857de6c81 fixed buggy if condition 2015-10-04 15:16:03 +01:00
Zachary Kincaid 9e34872e8f For ocamlfind install, set rpath to package directory if stublibs does not exist 2015-10-04 10:10:53 -04:00
Nikolaj Bjorner 459e456f66 disable memory finalization after quant_solve unit test. Related to issue #210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-03 17:37:33 -07:00
Nikolaj Bjorner 62a4737d77 disable code in dl_query that depends on hard-wired file path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-03 17:30:12 -07:00
Nikolaj Bjorner 50993582ec put break statement in else branh. Issue #230 (broken loop) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-03 17:15:54 -07:00
Nikolaj Bjorner 89f1541d83 put break statement in else branh. Issue #230 (broken loop) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-03 17:15:45 -07:00
Christoph M. Wintersteiger bcd3f56fa0 Merge branch 'pure' of https://github.com/Z3Prover/z3 2015-10-03 16:25:47 +01:00
Christoph M. Wintersteiger d8524ae4dd Fixed indentation 2015-10-03 16:24:06 +01:00
Christoph M. Wintersteiger 215f9d26eb Updated release notes 2015-10-02 20:07:42 +01:00
Christoph M. Wintersteiger 2397f37def Merge branch 'pure' of https://github.com/Z3Prover/z3 2015-10-02 19:55:22 +01:00
Christoph M. Wintersteiger 114f9834dd Adjusted copyright notice. 2015-10-02 19:51:06 +01:00
Christoph M. Wintersteiger 3b81118f4a Merge branch 'contrib' of https://github.com/Z3Prover/z3 2015-10-02 19:47:49 +01:00
Christoph M. Wintersteiger 95dea3922d Merge branch 'pure' of https://github.com/Z3Prover/z3 
Conflicts:
	src/api/ml/z3.ml
	src/api/ml/z3.mli
	src/api/python/z3util.py
 2015-10-02 19:47:24 +01:00
Christoph M. Wintersteiger a9d395ed7a Fixed comments about contributed code. 2015-10-02 19:45:33 +01:00
Christoph M. Wintersteiger 18a0314f6b Fix for ast_map in ML API 2015-10-02 15:52:33 +01:00
Christoph M. Wintersteiger e0026a1cbb Merge branch 'contrib' of https://github.com/Z3Prover/z3 2015-10-02 15:20:06 +01:00
Christoph M. Wintersteiger 0a95df8960 removed automatically generated file 2015-10-02 15:11:53 +01:00
Christoph M. Wintersteiger 08a3ab92f3 Added --noomp to mk_make 2015-10-02 12:38:56 +01:00
Christoph M. Wintersteiger 1294a2ac15 Fixed a memory leak 2015-10-01 13:31:37 +01:00
Nikolaj Bjorner 5d71190468 add catch for cancellation intermixed with return value l_true. To address regressions in QF_LIA tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-29 16:50:59 -07:00
Nikolaj Bjorner 77c423b9aa annotate enode hash as signed character to address issue #210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-29 14:14:29 -07:00
Nikolaj Bjorner 074ff58739 include rlimit in nlsat, include dedicated error message, for issue #216 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-29 09:27:34 -07:00
Nikolaj Bjorner d9b6623400 include rlimit in nlsat, include dedicated error message, for issue #216 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-29 09:16:46 -07:00
Christoph M. Wintersteiger 0cf18ab18e Propagated rlimit changes to sat::solver into sat_user_scope tests 2015-09-29 11:50:10 +01:00
Nikolaj Bjorner 1f9d5249a3 fix build break regarind z3test.py and added rlimit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 14:05:57 -07:00
Nikolaj Bjorner f3b8fe130a adding rlimit resource limit facility to provide platform and architecture independent method for canceling activities. This is to address issue #216 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 13:40:54 -07:00
Nikolaj Bjorner 9b3e242990 adding rlimit resource limit facility to provide platform and architecture independent method for canceling activities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 13:37:59 -07:00
Nikolaj Bjorner ad16cc0ce2 fix unit test for datalog parser, fixes issue #224 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 11:16:55 -07:00
Christoph M. Wintersteiger ac7e8b352f Improved support for UFs in FPA theory 2015-09-28 18:20:45 +01:00
Christoph M. Wintersteiger de3ead9ff1 build fix 2015-09-28 18:20:22 +01:00
Christoph M. Wintersteiger 076e680433 Improved UF suppport in fpa2bv_converter. 2015-09-25 17:28:31 +01:00
Christoph M. Wintersteiger 2744d80642 Fixed reference counting in fpa2bv converter. 2015-09-23 14:22:02 +01:00
Christoph M. Wintersteiger 04266fccc9 Bugfix for mpf sqrt. 
Fixes #222.
 2015-09-21 20:56:07 +01:00
Christoph M. Wintersteiger 0b15fc9402 Bugfix for mpf sqrt. 
Fixes #222.
 2015-09-21 19:44:53 +01:00
Christoph M. Wintersteiger d4b66538f9 Bug/assertion fix for power monomials in nlsat. 
Previously triggered an assertion on regressions/smt2/fp-to_real-1.smt2, but only on OSX and FreeBSD
 2015-09-17 16:31:51 +01:00
Christoph M. Wintersteiger 05d9e188f8 Reactivated smt.max_conflicts option. 
Partially fixes #216.
 2015-09-17 14:08:04 +01:00
Christoph M. Wintersteiger f3441c6a9b tabs and indentation 2015-09-17 13:25:22 +01:00
Christoph M. Wintersteiger d2c9b69eb3 fixed memory leak (`mem' remained allocated upon exception thrown in check_args). 2015-09-17 13:20:24 +01:00
Christoph M. Wintersteiger 2e071e89b0 tabs 2015-09-17 13:16:35 +01:00
Christoph M. Wintersteiger 4d39108808 Bugfix for fp.to_sbv 
Fixes #162
 2015-09-17 12:21:59 +01:00
Christoph M. Wintersteiger e9565d6a7f Fixed warning message 2015-09-17 12:18:44 +01:00
Christoph M. Wintersteiger 2115ea8bb8 Bugfix for fp.sqrt. 
Fixes #220.
 2015-09-17 12:13:04 +01:00
Christoph M. Wintersteiger 52df2224e9 Disabled FP debug variables. 2015-09-16 18:04:26 +01:00
Christoph M. Wintersteiger 27f8ad288c Bugfix for fp.to_ubv. 
Fixes #162.,
 2015-09-16 14:26:53 +01:00
Christoph M. Wintersteiger 79d69cd5f0 Added FP to_ieee_bv to fpa_rewriter to enable model evaluation. 2015-09-16 12:57:05 +01:00