mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity
404 commits 23 branches 48 tags 156 MiB
Commit graph

404 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura b472a36b42 added --staticlib option to mk_make.py 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-14 09:03:13 -08:00
Leonardo de Moura ead762e0d0 bumped version number 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-14 09:02:53 -08:00
Leonardo de Moura 79eca95a95 bumped version number 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 22:46:57 -08:00
Leonardo de Moura 89c1785b73 fixed clang++ for linux 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 21:49:37 -08:00
Leonardo de Moura ad3aa96726 improving clang++ support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 21:26:28 -08:00
Leonardo de Moura 3e8d3db290 fixed gcc compilation error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 09:26:01 -08:00
Leonardo de Moura b335661d5a Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-13 09:17:35 -08:00
Leonardo de Moura 50e00b615f updated release notes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 09:16:51 -08:00
Leonardo de Moura f9ec1f2a63 making sure par-or and par-then combinators work correctly even when OpenMP is not available 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 09:14:36 -08:00
Leonardo de Moura 8ad12a7dd4 Missing config option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 09:14:02 -08:00
Nikolaj Bjorner 68ae5d434c fix cover retrieval for slicing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-13 17:00:01 +01:00
Leonardo de Moura 854641c8db updated RELEASE_NOTES 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-11 22:09:51 -08:00
Leonardo de Moura 00dbe92cea polishing clang++ support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-11 22:05:17 -08:00
Leonardo de Moura 504ba8236d added support for clang++ on Linux 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-11 21:42:36 -08:00
Leonardo de Moura ed6e688b94 updated RELEASE_NOTES. fixed mk_make.py 2012-11-11 21:06:17 -08:00
Leonardo de Moura e0fcbc101c Added support for clang++ on OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-12 04:56:48 +00:00
Leonardo de Moura 99b7f7509d bump version number in unstable branch 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-11 10:50:24 -08:00
Leonardo de Moura a6db55d21f Display version number using new format 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-10 19:03:16 -08:00
Leonardo de Moura caced62f40 New API for adding 'tracked assertions'. Added wrappers for creating existential and universal quantifiers in the C++ API fronted. Added new examples for the C++ API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-10 15:54:31 -08:00
Nikolaj Bjorner 108bbb0597 add missing check for difference logic fragment for clause heads 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-10 11:50:17 +01:00
Leonardo de Moura a5ceff98ea cleaned exampled 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-08 07:11:22 -08:00
Leonardo de Moura 1cf8d61def new example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-08 07:00:27 -08:00
Leonardo de Moura 73a13f209b fixed bug detected in regression tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-07 10:46:00 -08:00
Leonardo de Moura c5b91aef68 Fixed bug reported by Heizmann at codeplex 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-07 07:52:07 -08:00
Leonardo de Moura 8d6a091083 fixed bugs found in regression tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-07 07:36:40 -08:00
Leonardo de Moura c3a0a29c4f fixed problem with Python 2.5 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-07 05:55:41 -08:00
Nikolaj Bjorner cec851440e fix model completion bug in PDR, addhoc handling of reals for arithmetic realizers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-06 15:38:07 +02:00
Leonardo de Moura 2c66afadd6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-04 12:49:58 -08:00
Leonardo de Moura 10b95de82e resurrected test/quant_elim.cpp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-04 12:49:33 -08:00
Nikolaj Bjorner 5ef505c357 set model completion to force value computation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-04 14:22:56 +02:00
Nikolaj Bjorner 37a13b1d09 update slicing to fix unbound variables. test datatype realizer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-04 14:15:24 +02:00
Nikolaj Bjorner bfbdad3ce6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-04 08:40:23 +02:00
Nikolaj Bjorner 927dc2e490 fix if-lifting, added light-weight FM to qe_lite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-04 08:40:16 +02:00
Leonardo de Moura 6580a83594 minor fix for ramdisk build 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 21:16:52 -07:00
Leonardo de Moura c1587dc37d fixed some warnings reported by clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 17:28:27 -07:00
Leonardo de Moura ed52dce9b0 Merge branch 'solver_na2as' into unstable 2012-11-02 16:35:23 -07:00
Leonardo de Moura b70687acc9 cleanning solver initialization, and fixing named assertion support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 16:35:08 -07:00
Leonardo de Moura 181bdb6815 removed dead files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 14:18:12 -07:00
Leonardo de Moura e2f6a65aa2 added support for named assertions 2012-11-02 14:00:43 -07:00
Leonardo de Moura e08c569d8d new qe example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 12:04:02 -07:00
Leonardo de Moura e1eb3ee8ee fixed bug in solver_na2as 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 11:36:59 -07:00
Leonardo de Moura 33c165490c fixed solver_na2as 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 09:43:07 -07:00
Leonardo de Moura d545f187f8 working on named assertions support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 08:28:34 -07:00
Leonardo de Moura 230382d4c9 default_solver --> smt_solver 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-01 21:52:27 -07:00
Leonardo de Moura cadd35bf7a checkpoint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-01 21:44:35 -07:00
Leonardo de Moura adb6d05805 fixed typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-01 14:43:02 -07:00
Leonardo de Moura 398f1b1de1 moving assertion_stack to mcsat branch 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-01 13:29:09 -07:00
Leonardo de Moura c096fb534b checkpoint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-01 13:28:10 -07:00
Nikolaj Bjorner 4f2b7049ab Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-01 13:06:16 -07:00
Nikolaj Bjorner 1c17e40fe5 optmizing DL 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-01 13:06:10 -07:00