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

1291 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger 210bca8f45 .NET Example: Sudoku example bugfix. Many thanks to Ilya Mironov for reporting this issue. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-07-02 12:57:54 +01:00
Leonardo de Moura b7c2d9054b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-28 19:21:34 -07:00
Leonardo de Moura d9941c0ccc Add code for rejecting bitvector constants of size 0 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-28 19:21:27 -07:00
Christoph M. Wintersteiger 9dfd202fdb Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-28 12:14:33 +01:00
Christoph M. Wintersteiger 4f72e1d528 FPA: avoid compiler warnings. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-28 12:14:14 +01:00
Nikolaj Bjorner d9e3881560 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-27 12:00:09 -05:00
Nikolaj Bjorner 619bd91ddb fix bug in ctx-solver-simplify reported @ http://z3.codeplex.com/workitem/51 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-27 11:59:40 -05:00
Leonardo de Moura 544dfde454 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-27 09:30:33 -07:00
Leonardo de Moura 5b7201a911 Fix minor problem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-27 09:30:25 -07:00
Leonardo de Moura f238720b76 Cherry-pick goodies from mcsat branch 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-27 09:19:23 -07:00
Christoph M. Wintersteiger 42b3a81ef6 FPA: precision bugfixes for FMA 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-27 16:08:25 +01:00
Christoph M. Wintersteiger 0d2a7f922c FPA: sqrt precision bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-26 18:16:25 +01:00
Nikolaj Bjorner 13262a0fc5 missing files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-25 13:13:47 -05:00
Nikolaj Bjorner 324dc5869d fix substitution bug in qe, working on boogie trace 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-25 13:07:28 -05:00
Christoph M. Wintersteiger 67aaec872a Java API: status bugfix. Thanks to user Bauna for reporting this 
issue (#50).

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-25 18:27:53 +01:00
Christoph M. Wintersteiger 56b41a0065 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 
+ FPA2BV sqrt fix

Conflicts:
	src/tactic/fpa/fpa2bv_converter.cpp

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-25 16:34:38 +01:00
Christoph M. Wintersteiger 74792eeec4 FPA: compilation bugfixes 2013-06-25 15:06:13 +01:00
Christoph M. Wintersteiger a9c4470a6b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-25 14:53:28 +01:00
Leonardo de Moura 205520ed6c Move AssemblyInfo.cs AssemblyInfo. Update mk_util.py to generate AssemblyInfo.cs instead of modifying it. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-24 15:34:42 -07:00
Christoph M. Wintersteiger 127402c10b FPA: fpa2bv fma bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-24 16:33:09 +01:00
Christoph M. Wintersteiger 9581055f97 FPA: debug output disabled 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-24 13:30:36 +01:00
Christoph M. Wintersteiger 13206f2fe7 FPA: FMA bugfixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-24 13:29:04 +01:00
Nikolaj Bjorner 5b5a474b54 experiment with point-based generalization method 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-21 16:23:37 -07:00
Christoph M. Wintersteiger 9489c9b08b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-21 21:16:12 +01:00
Christoph M. Wintersteiger 0b6250253a FPA2BV: added sqrt function 
(Currently, there are a few corner cases where it doesn't round correctly.)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-21 21:16:03 +01:00
Leonardo de Moura 42898f3276 Fix bug reported by Florian <corzilius@cs.rwth-aachen.de> 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-21 10:31:11 -07:00
Leonardo de Moura a60b53bfd8 Fix compilation errors/warnings when using GCC 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-20 17:52:20 -07:00
Leonardo de Moura f5f04e583b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-20 17:48:57 -07:00
Leonardo de Moura 185f125f7a Fix problem reported at http://stackoverflow.com/questions/17215640/getting-concrete-values-from-a-model-containing-array-ext 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-20 17:48:43 -07:00
Leonardo de Moura cd485f03dd Add trace msg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-20 17:02:15 -07:00
Christoph M. Wintersteiger ecceb0accc FPA: debug output disabled. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 20:16:02 +01:00
Christoph M. Wintersteiger 92c1b25978 FPA: bugfix for float to float conversion (subnormal numbers). 
Thanks to Gabriele Paganelli for reporting this bug!

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 20:14:00 +01:00
Christoph M. Wintersteiger 76c59cb85c MPF conversion bugfix. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 17:22:25 +01:00
Christoph M. Wintersteiger 1a26c9726b .NET API: bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 13:15:48 +01:00
Leonardo de Moura 894fd8b967 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-13 13:45:55 -07:00
Leonardo de Moura 40b1137b30 Fix issue https://z3.codeplex.com/workitem/47 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-13 13:45:14 -07:00
Leonardo de Moura 2c8b314a15 Fix issue https://z3.codeplex.com/workitem/48 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-13 13:34:20 -07:00
Nikolaj Bjorner 6184c5fdbc reorder attibutes to match initialization order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-11 15:29:22 -04:00
Nikolaj Bjorner 0210156bf0 add convex interior generalizer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-10 10:51:56 -04:00
Christoph M. Wintersteiger 455618bb2b FPA: added is_nan 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 18:34:31 +01:00
Christoph M. Wintersteiger d7639557d2 FPA: added rewriting and fpa2bv conversion rules for new operations. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 18:03:46 +01:00
Christoph M. Wintersteiger 123d3ec3a7 New FPA operators added. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 17:55:29 +01:00
Christoph M. Wintersteiger e5c720de29 FPA: bugfix for abs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 17:36:34 +01:00
Christoph M. Wintersteiger 724f2af8c7 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-07 17:34:38 +01:00
Leonardo de Moura 2b59f2ecc2 Fix issue https://z3.codeplex.com/workitem/37 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-06 18:29:29 -07:00
Leonardo de Moura f4f1c63abb Fix issue https://z3.codeplex.com/workitem/38 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-06 13:20:43 -07:00
Leonardo de Moura 110fa0b7fb Fix issue http://z3.codeplex.com/workitem/45 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-05 13:50:22 -07:00
Christoph M. Wintersteiger d301bd35a9 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-05 14:36:18 +01:00
Nikolaj Bjorner b6d9d8a601 fix bugs reported by Nuno Lopes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-04 12:55:35 -07:00
Nikolaj Bjorner aa0d921240 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-03 11:48:21 -07:00