mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
4730 commits 49 branches 53 tags 182 MiB
Commit graph

4730 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
19c22fde50 Merge branch 'pure' of https://github.com/Z3Prover/z3 2015-10-04 16:42:07 +01:00
Christoph M. Wintersteiger
f11502e0ac reinterpret_cast fixes for the Windows compiler. 2015-10-04 16:41:28 +01:00
Christoph M. Wintersteiger
ceb562a889 Merge branch 'pure' of https://github.com/Z3Prover/z3 2015-10-04 16:05:25 +01:00
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