mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
1622 commits 49 branches 53 tags 182 MiB
Commit graph

1622 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
07d56bdc70 Java API bugfixes for cygwin compilation 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-02-21 13:44:39 +00:00
Christoph M. Wintersteiger
d51d9b18f9 Bugfixes for compilation in Cygwin (WIN32 -> _WINDOWS) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-02-21 13:00:02 +00:00
Leonardo de Moura
e077fc5cb4 fix(api/python): make sure Z3 compiles using Python3 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-20 14:09:55 -08:00
Ken McMillan
75bb495585 merging interpolation and duality changes into unstable 2014-02-19 15:36:16 -08:00
Ken McMillan
65c54b87d0 duality fix 2014-02-19 13:57:27 -08:00
Ken McMillan
c9cf658e7c interpolation fix for commutativity 2014-02-19 13:56:55 -08:00
Ken McMillan
76fb66314b interpolation fix for commutativity 2014-02-19 13:56:16 -08:00
Andreas Froehlich
25378f7989 some extensions/modifications. versions added. 2014-02-18 14:01:47 +00:00
Ken McMillan
928d419138 duality fixes 2014-02-17 12:15:11 -08:00
Ken McMillan
cb3dc63e68 some interpolation fixes; make duality a bit more persistent in checking interpolant 2014-02-14 15:52:07 -08:00
Ken McMillan
88ff20a0fb fixed multiple interpolation bugs 2014-02-14 15:48:38 -08:00
Christoph M. Wintersteiger
e860c65567 bugfix for sign computation in floating-point FMA 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-02-13 19:33:51 +00:00
Andreas Froehlich
87c6fc66d6 sls tactic default 2014-02-11 17:44:59 +00:00
Ken McMillan
f45ad4bdc0 disable silly warnings and add needed header for VS 2014-02-10 12:56:39 -08:00
Ken McMillan
ba193a59b1 some interpolation fixes, plus some options to remove features for testing in duality 2014-02-09 16:04:02 -08:00
Ken McMillan
19830bcd33 fix a few warnings 2014-01-28 11:43:00 -08:00
Ken McMillan
466c35100d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-01-28 11:28:24 -08:00
Christoph M. Wintersteiger
f111dd4e61 Fixes for the build on OS X 10.9 2014-01-28 14:00:42 +00:00
Christoph M. Wintersteiger
0e74362ecb Added support for the final draft of the FPA standard (and fpa2bv conversion). 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-01-24 15:36:23 +00:00
Christoph M. Wintersteiger
b2be81fd4d bugfix for OSX build configuration 2014-01-22 13:41:48 +00:00
Christoph M. Wintersteiger
73a1dddc45 Bugfixes for the build on new OSX machines (XCode 5.0 on). 2014-01-21 17:06:13 +00:00
Nikolaj Bjorner
d548c51a98 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-01-13 13:42:15 -08:00
Nikolaj Bjorner
b80302cfb0 generalize guard in conflict resolution to handle non-equality binary predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-13 13:41:47 -08:00
Nikolaj Bjorner
da4793de76 fix type checking bug reported by Nate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-09 21:14:30 -08:00
Ken McMillan
f380e31a6b runs the integer/cntrol svcomp examples from the Horn repo 2014-01-09 17:16:10 -08:00
Nikolaj Bjorner
084a6f35eb fix bug reported by Nuno Lopes: inlining is unsound for negated predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-02 17:37:35 -08:00
Nikolaj Bjorner
81f1f7690d fix bug in rational.is_int32, it recognized rationals; fix bug reported by Anvesh for integer arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-31 15:59:56 -08:00
Ken McMillan
11ba2178a9 speeding up interpolation in RPFP_caching 2013-12-24 17:20:12 -08:00
Ken McMillan
1b9f1ea6b3 remove assert on failed label compuation in duality 2013-12-23 11:47:24 -08:00
Ken McMillan
673ba137e5 added qe_lite preprocessing pass to duality 2013-12-23 11:17:38 -08:00
Ken McMillan
9e88691c69 optimizing solver performance in duality 2013-12-22 18:33:40 -08:00
Ken McMillan
c98b853917 speeding up Generalize and adding Lazy Propagation 2013-12-21 16:54:35 -08:00
Ken McMillan
48e10a9e2d dealing with incompleteness issues in duality 2013-12-19 11:05:56 -08:00
Nikolaj Bjorner
0d6220f383 revert is_all_int bugfix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-18 21:53:04 +02:00
Christoph M. Wintersteiger
8fb36bd41d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-12-17 13:53:28 +00:00
Christoph M. Wintersteiger
0b3e50d6e6 Added #include <algorithm> because VS2013 needs that for std::max/std::min 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-12-17 13:53:10 +00:00
Ken McMillan
a318b0f104 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-12-16 12:45:52 -08:00
Ken McMillan
3588d4a1ca fixing templates for broken windows hash functions 2013-12-16 12:41:43 -08:00
Ken McMillan
1e8c04be8e fixing templates for broken windows hash functions 2013-12-15 17:31:46 -08:00
Ken McMillan
852f53d6a6 fixed memory error 2013-12-15 17:24:51 -08:00
Ken McMillan
ebc8a43fe3 removing address dependencies 2013-12-15 15:49:06 -08:00
Nikolaj Bjorner
909408d6ef fix is_all_int bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 10:58:23 +02:00
Ken McMillan
eee2d7af94 porting to linux 2013-12-14 12:47:02 -08:00
Ken McMillan
3764064e98 fixed some address dependencies 2013-12-13 18:41:35 -08:00
Ken McMillan
bb61f17989 trying to figure out address dependency 2013-12-13 13:45:40 -08:00
Ken McMillan
ac9a7748e8 trying to fix address depedency in duality_solver.cpp 2013-12-13 13:14:04 -08:00
Ken McMillan
0449598530 fussing more with qe in duality 2013-12-13 12:41:51 -08:00
Ken McMillan
a410e7f716 fussing with qe in duality 2013-12-13 12:21:54 -08:00
Ken McMillan
bfa6c99676 still trying to get stl to work 2013-12-12 18:38:09 -08:00
Ken McMillan
cf3ede92ad fix for broken windows stl 2013-12-12 18:35:43 -08:00