mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-27 09:49:23 +00:00
Code Activity
4027 commits 45 branches 52 tags 177 MiB
Commit graph

4027 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
df1f600624 Merge branch 'daniel-j-h-buildsystem_cleanup' 2015-10-19 15:18:52 +01:00
Christoph M. Wintersteiger
b1fcdadd55 Merge branch 'buildsystem_cleanup' of https://github.com/daniel-j-h/z3 into daniel-j-h-buildsystem_cleanup 2015-10-19 15:18:13 +01:00
Christoph M. Wintersteiger
6749c19ab1 Merge branch 'static_analysis' of https://github.com/daniel-j-h/z3 
# Conflicts:
#	src/ast/ast.h
#	src/interp/iz3foci.cpp
#	src/muz/duality/duality_dl_interface.cpp
#	src/util/hwf.h
 2015-10-19 15:14:45 +01:00
Christoph M. Wintersteiger
954a629296 Merge branch 'zkincaid-uint' 2015-10-19 15:01:07 +01:00
Christoph M. Wintersteiger
059c58e6d8 Merge branch 'uint' of https://github.com/zkincaid/z3 into zkincaid-uint 2015-10-19 15:00:43 +01:00
Christoph M. Wintersteiger
0c774e59c3 Merge branch 'Dmitriy403-WpedanticFix' 2015-10-19 14:57:49 +01:00
Christoph M. Wintersteiger
57db321daf Merge branch 'WpedanticFix' of https://github.com/Dmitriy403/z3 into Dmitriy403-WpedanticFix 2015-10-19 14:57:34 +01:00
Christoph M. Wintersteiger
9d505ec7ff Merge branch 'unstable' of https://github.com/jmgrosen/z3 into jmgrosen 2015-10-19 14:53:06 +01:00
Christoph M. Wintersteiger
1364f39f61 Merge pull request #218 from cgcgbcbc/fix/implies 
fix implies(expr const &, expr const &) in z3++.h
 2015-10-19 14:29:07 +01:00
Christoph M. Wintersteiger
d4e0de8f84 Merge pull request #234 from martin-neuhaeusser/master 
Fixed typo that accidentally prints warning message if a Z3 context i…
 2015-10-19 14:24:35 +01:00
Christoph M. Wintersteiger
6e8c035b7f Merge branch 'npricci-master' 2015-10-19 14:23:04 +01:00
Christoph M. Wintersteiger
bd3775e878 Merge branch 'master' of https://github.com/npricci/z3 into npricci-master 
# Conflicts:
#	src/api/python/z3.py
 2015-10-19 14:22:56 +01:00
Christoph M. Wintersteiger
3c89312d1e Merge pull request #55 from zshipko/master 
support openbsd
 2015-10-19 14:15:56 +01:00
Christoph M. Wintersteiger
536c70df14 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-19 14:10:35 +01:00
Christoph M. Wintersteiger
87028e8931 Merge branch 'benlaurie-sudoku-in-c++' 2015-10-19 14:09:47 +01:00
Christoph M. Wintersteiger
a6f85f3932 Merge branch 'sudoku-in-c++' of https://github.com/benlaurie/z3 into benlaurie-sudoku-in-c++ 
# Conflicts:
#	examples/c++/example.cpp
 2015-10-19 14:09:36 +01:00
Christoph M. Wintersteiger
b9f66c545a Merge pull request #11 from Confusion/patch-1 
Corrected typo: interger -> integer
 2015-10-19 14:07:02 +01:00
Christoph M. Wintersteiger
ef80645a71 Java API context deletion concurrency fix. 
Relates to #205 #245
 2015-10-14 22:13:43 +01:00
Christoph M. Wintersteiger
a71a333722 Minor Java API fix. 2015-10-14 21:33:30 +01:00
Christoph M. Wintersteiger
2d3c12716a Bugfix for Java memory leaks. 
Relates to #205 #245
 2015-10-14 21:19:59 +01:00
Christoph M. Wintersteiger
58d3329190 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-14 13:59:20 +01:00
Christoph M. Wintersteiger
24532474a0 Bugfix for concurrent Context creation in Java and .NET. 
Relates to #205 #245
 2015-10-14 13:58:51 +01:00
Christoph M. Wintersteiger
d48b25f38b Merge pull request #246 from wintersteiger/java_fix 
Java fix
 2015-10-14 12:59:26 +01:00
Christoph M. Wintersteiger
b66f34f0d2 Removed unnecessary debug output. 2015-10-14 12:53:18 +01:00
Christoph M. Wintersteiger
bae3a76c8a Removed unnecessary debug output. 2015-10-14 12:52:16 +01:00
Christoph M. Wintersteiger
5e0470f5a3 Merge branch 'master' of https://github.com/Z3Prover/z3 into java_fix 2015-10-14 12:43:49 +01:00
Christoph M. Wintersteiger
e312b47be6 Bugfix for object finalization in Java API. 
Relates to #205 and #245
 2015-10-14 12:43:09 +01:00
Christoph M. Wintersteiger
6263252bf5 Bugfix for concurrent garbage collection in Java API. 
Relates to #205 and #245
 2015-10-14 12:42:27 +01:00
Nikolaj Bjorner
0a75ba0322 Merge pull request #244 from NikolajBjorner/master 
fix for fixed size rational difference logic
 2015-10-13 09:46:01 -07:00
Nikolaj Bjorner
f4954e9d7f fix for fixed size rational difference logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-13 09:24:02 -07:00
Christoph M. Wintersteiger
2d2ec38541 Merge pull request #238 from nunoplopes/master 
use Z3_fallthrough instead of __falthrough directly
 2015-10-09 18:42:26 +01:00
Nuno Lopes
0e387b2abe use Z3_fallthrough instead of __falthrough directly to avoid messing with reserved identifiers 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-10-09 18:06:49 +01:00
Christoph M. Wintersteiger
a951ff0769 Fix for FP UFs and conversion functions. 2015-10-08 16:04:17 +01:00
Christoph M. Wintersteiger
883514c195 Bugfix for FPA UFs 2015-10-08 14:14:39 +01:00
Christoph M. Wintersteiger
c787ea1a3b Bugfix for FP UFs. 2015-10-08 12:45:26 +01:00
Christoph M. Wintersteiger
a2503af585 Bugfixes for UFs and conversion functions in theory_fpa 2015-10-08 11:54:35 +01:00
Christoph M. Wintersteiger
b60f30c802 Merge pull request #236 from wintersteiger/i68 
Fixes for issue #68
 2015-10-07 20:56:35 +01:00
Christoph M. Wintersteiger
06675e6e70 Merge pull request #235 from wintersteiger/fpa_fixes 
Bugfix for mpf to_ieee_bv
 2015-10-07 20:46:47 +01:00
Christoph M. Wintersteiger
de39173f6f Corrected unspecified behavior of fp.min/fp.max corner cases in fpa2bv_converter and in theory_fpa. 
Fixes #68
 2015-10-07 20:44:08 +01:00
Christoph M. Wintersteiger
8a026c355f Corrected unspecified behavior of corner cases in fp.min/fp.max. 
Partially addresses #68.
 2015-10-07 20:39:36 +01:00
Christoph M. Wintersteiger
76540d13d6 Merge branch 'fpa_fixes' of https://github.com/wintersteiger/z3 into fpa_fixes 2015-10-07 20:37:34 +01:00
Christoph M. Wintersteiger
fcf036695e Bugfix for mpf to_ieee_bv 2015-10-07 20:37:12 +01:00
Christoph M. Wintersteiger
f2ff071224 Bugfix for mpf to_ieee_bv 2015-10-07 20:17:04 +01:00
martin-neuhaeusser
99e4b321bd Fixed typo that accidentally prints warning message if a Z3 context is created with the 'timeout' parameter 2015-10-07 17:27:05 +02:00
Nikolaj Bjorner
6e852762ba patch for issue #232 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-06 19:07:47 -07:00
Nikolaj Bjorner
773f90f122 add to release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-05 09:31:14 -07:00
Christoph M. Wintersteiger
115187ee2b Bumped version number to 4.4.2. 2015-10-05 16:04:03 +01:00
Christoph M. Wintersteiger
95c9ccb295 Merge branch 'pure' of https://github.com/Z3Prover/z3 2015-10-05 13:07:19 +01:00
Nikolaj Bjorner
7b95d6894a comment out unit test that depends on hard-wired path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-04 16:34:23 -07:00
Christoph M. Wintersteiger
8e2ec55af4 Merge branch 'pure' of https://github.com/Z3Prover/z3 2015-10-04 23:37:18 +01:00