mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity
2560 commits 23 branches 48 tags 157 MiB
Commit graph

2560 commits

This branch
This branch
All branches
Author SHA1 Message Date
Daniel J. Hofmann
4b6b718222 Wunused-exception-parameter 2015-04-03 20:11:58 +02:00
Daniel J. Hofmann
2252836cf8 Wstring-conversion 
static_cast<bool>("string lit") evaluates to true. The assert is
supposed to always trigger, thus assert(false && "string lit").
 2015-04-03 19:55:21 +02:00
Daniel J. Hofmann
42e0132639 Wshift-sign-overflow 
See:
http://stackoverflow.com/questions/26331035/why-was-1-31-changed-to-be-implementation-defined-in-c14

And Howard Hinnant's explanation:
http://stackoverflow.com/questions/19593938/is-left-shifting-a-negative-integer-undefined-behavior-in-c11#comment29091986_19593938
 2015-04-03 19:45:49 +02:00
Daniel J. Hofmann
88f6e74a27 Wnewline-eof 2015-04-03 19:31:09 +02:00
Daniel J. Hofmann
6150083276 Wignored-qualifiers 2015-04-03 19:24:35 +02:00
Daniel J. Hofmann
4e59ba922b Wc++11-extensions 2015-04-03 19:13:52 +02:00
Nikolaj Bjorner
d01c3491a6 simplify with caching, but without expanding number of asserted formulas. Bug reported by Heizmann, codeplex issue 197 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-02 10:28:30 -07:00
Christoph M. Wintersteiger
70d765df5c Merge pull request #23 from wintersteiger/unstable 
Made GetInterpolant and ComputeInterpolant public in Java and .NET.
 2015-04-02 17:53:34 +02:00
Christoph M. Wintersteiger
b47851d7da Made GetInterpolant and ComputeInterpolant public in Java and .NET. 
Fixes Codeplex discussion #616450
 2015-04-02 16:51:30 +01:00
Christoph M. Wintersteiger
7fe337daef Merge pull request #21 from wintersteiger/unstable 
Made the InterpolationContext public.
 2015-03-31 19:53:10 +02:00
Christoph M. Wintersteiger
1d9c9bcf7a Made the InterpolationContext public. 
Fixes #20
 2015-03-31 19:51:42 +02:00
Christoph M. Wintersteiger
637554dcf5 Merge pull request #18 from wintersteiger/unstable 
Bugfix for mpf is_normal.
 2015-03-30 10:29:54 +01:00
Christoph M. Wintersteiger
99ea0a8c19 Bugfix for mpf is_normal. 
Fixes #17
 2015-03-30 08:02:57 +01:00
Christoph M. Wintersteiger
5540d738ab Merge pull request #16 from wintersteiger/unstable 
Enabled test for OpenMP in Windows (for old and express versions of visu...
 2015-03-29 15:56:50 +01:00
Christoph M. Wintersteiger
0f03cd2ae0 Enabled test for OpenMP in Windows (for old and express versions of visual studio). 
Fixes #8
 2015-03-29 15:49:03 +01:00
Christoph M. Wintersteiger
4a0eb93f87 Merge pull request #15 from wintersteiger/unstable 
Integrating fixes for #10, #13, #14
 2015-03-29 14:44:21 +01:00
Christoph M. Wintersteiger
5911f788c3 Improved translation from reals to floats (fp.to_real). 
Fixes #14
 2015-03-29 14:39:47 +01:00
Christoph M. Wintersteiger
0ed16c09f9 Bugfix for fp.isNegative. 
Fixes #13
 2015-03-29 13:57:11 +01:00
Christoph M. Wintersteiger
690eb8eaca Bugfix for fp.isSubnormal. 
Fixes #10
 2015-03-29 13:31:44 +01:00
Nikolaj Bjorner
4bfe20647b remove tab in mk_util.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-27 02:43:21 -07:00
Nikolaj Bjorner
e456af142e fix complex.py example with power prompted by suggestion of smilliken 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-27 02:42:08 -07:00
NikolajBjorner
3b16cfbd44 Update README 
change reference to license
 2015-03-26 11:43:51 -07:00
Leonardo de Moura
274f2b7a5d Move to MIT License 2015-03-26 11:43:41 -07:00
Christoph M. Wintersteiger
fc84461e31 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-03-26 14:49:45 +00:00
Christoph M. Wintersteiger
9cbf45f689 Added int to float conversion. 2015-03-26 14:48:55 +00:00
Nikolaj Bjorner
0482e7fe72 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:46:28 -07:00
Nikolaj Bjorner
39892aae10 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:46:17 -07:00
Nikolaj Bjorner
8059a5a0b7 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:36:01 -07:00
Nikolaj Bjorner
86ac20faf6 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:35:44 -07:00
Nikolaj Bjorner
3c5897eea0 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-03-25 11:25:12 -07:00
Nikolaj Bjorner
2aa91eee70 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:24:47 -07:00
Christoph M. Wintersteiger
a792790882 Fixed performance problems with enumeration sorts (Codeplex #190). 2015-03-25 18:08:56 +00:00
Christoph M. Wintersteiger
1c77ad00c3 Added accessors to enumeration sorts. Thanks to codeplex user steimann for suggesting this. 
(http://z3.codeplex.com/workitem/195)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-24 21:42:05 +00:00
Christoph M. Wintersteiger
b76d588c28 Renamed the soft_timeout option to just timeout. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-21 16:10:30 +00:00
Ken McMillan
be709802cd merging interpolation fix (issue 182) 2015-03-20 17:46:01 -07:00
Ken McMillan
47d33452c6 interpolation fix (issue 182) 2015-03-20 17:39:45 -07:00
Christoph M. Wintersteiger
ed81e3b9d8 Bugfix for BV-SLS initialization 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-20 17:07:32 +00:00
Nuno Lopes
4ed062d54a fix missing memset in my previous commit 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-03-11 11:04:33 +00:00
Nikolaj Bjorner
695ce643f5 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-03-11 00:45:09 -07:00
Nikolaj Bjorner
755a259ea0 fix codeplex issue 188 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-11 00:44:56 -07:00
Nuno Lopes
44e647e72b add reallocate() function and use it in bit_vector and vector containers 
give a speedup of 1-4%

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-03-10 16:53:47 +00:00
Christoph M. Wintersteiger
55ca6ce44b Resurrected the dack* options. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-04 19:15:22 +00:00
Christoph M. Wintersteiger
6630994a3d + bug reporter 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-04 18:31:08 +00:00
Christoph M. Wintersteiger
858ce1158d Bugfix in model translation (ast_manager mismatch after par-or). Thanks to stackoverflow user user297886 for reporting this issue. 
http://stackoverflow.com/questions/28852722/segmentation-fault-while-using-par-or-tactic
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-04 18:30:06 +00:00
Christoph M. Wintersteiger
8d11c431b7 Bugfix for the OCaml bindings on Windows 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-04 17:44:53 +00:00
Christoph M. Wintersteiger
ec4a07318e Bugfix for the Java API on Windows 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-04 15:19:15 +00:00
Christoph M. Wintersteiger
1f8119f601 Bugfix for the Java API. Thanks to codeplex user susmitj for reporting this problem! 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-04 15:14:07 +00:00
Christoph M. Wintersteiger
400e203bce Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-02 17:31:42 +00:00
Christoph M. Wintersteiger
71f2d358ef Bugfix in windows dist scripts 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-02 17:30:41 +00:00
Nuno Lopes
dd2c179663 Fix warnings during compilation with MSVC due to /LTCG 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-03-02 15:05:38 +00:00