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

1874 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes 1a396b0bd2 [BV size reduction] fix bug in detection of signed upperbound 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-11-25 18:13:24 +00:00
Christoph M. Wintersteiger 59dfd2abe4 fixed problem with Python 3.4.x complainging of inconsistent use of spaces/tabs. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-11-25 14:54:47 +00:00
Christoph M. Wintersteiger 53cfa47214 bugfix for bv_size_reduction 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-11-25 14:22:50 +00:00
Christoph M. Wintersteiger 213d816c0a Bugfix for bv_size_reduction. Thanks to user rsas for reporting this isse! 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-11-24 18:10:54 +00:00
Nikolaj Bjorner 4c5753f321 be classy with your friends 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-11-13 18:08:24 -08:00
Nikolaj Bjorner 025d6c3108 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-11-12 20:28:36 -08:00
Nikolaj Bjorner a309dbfdc2 coerce equality and ite upward instead of downward for int2real coercions. Fixes bug reported by Enric Carbonell 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-11-12 20:28:11 -08:00
Christoph M. Wintersteiger 005bb82a17 eliminated unused variables 2014-11-07 16:04:02 +00:00
Nikolaj Bjorner cf8ad072d0 remove unused variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-11-07 16:03:27 +01:00
Nikolaj Bjorner ce7303b5e2 fix reset logic and load only logics admitted by context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-11-07 15:44:21 +01:00
Nikolaj Bjorner 23bc982ad2 move initialization to support more sort usage scenarios 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-11-06 16:53:51 +01:00
Nikolaj Bjorner adeae18471 delay initializing internal manager so that parser does not choke on proper SMT-LIB logics. Reported by Venkateshan 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-11-06 13:09:25 +01:00
Christoph M. Wintersteiger 591f6d096f .NET API project directories fixed. Thanks to Marc Brockschmidt for reporting this. 2014-11-03 14:53:48 +00:00
Nikolaj Bjorner e002fc680f Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-31 14:24:35 +01:00
Nikolaj Bjorner b4600ffda0 add print to SMT-LIB format from solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-31 14:24:21 +01:00
Christoph M. Wintersteiger f50a8b0a59 Bumped version number. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-25 17:05:02 +01:00
Christoph M. Wintersteiger 6b51f7a610 Added item to release notes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-25 16:59:24 +01:00
Christoph M. Wintersteiger cb3e9c9644 Bugfix for FPA models 2014-10-25 16:58:16 +01:00
Christoph M. Wintersteiger 0713535fa6 Documentation website fixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 21:00:23 +01:00
Ken McMillan 61905a10db merge interp change 2014-10-24 11:54:00 -07:00
Ken McMillan da71d5ee01 unlimit stack on linux/mac 2014-10-24 11:53:03 -07:00
Christoph M. Wintersteiger ddebb4a69d Documentation fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 19:45:21 +01:00
Christoph M. Wintersteiger 2f9b3c42eb Java API cleanup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 19:43:36 +01:00
Christoph M. Wintersteiger 60cf1d5a4f Update copyright notices 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 18:02:58 +01:00
Christoph M. Wintersteiger cc99e96786 Java API Cleanup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 18:00:36 +01:00
Christoph M. Wintersteiger 6e159bd442 updated release notes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 15:54:49 +01:00
Christoph M. Wintersteiger 4d62ff6b9f Spelling. Thanks to codeplex user regehr for reporting this. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 15:53:52 +01:00
Christoph M. Wintersteiger e0c42f5892 Java API bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 14:43:01 +01:00
Christoph M. Wintersteiger 7d196201dc fixed warnings 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 12:33:20 +01:00
Christoph M. Wintersteiger fd0920eb36 Updated release notes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-23 19:15:26 +01:00
Christoph M. Wintersteiger 6a27d93776 Fixed memory leaks in interpolation API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-23 17:20:55 +01:00
Christoph M. Wintersteiger a6bee82ef8 Interpolation API: fixed some memory leaks 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-23 17:10:31 +01:00
Nuno Lopes 5adfbe8857 Z3Py: Fix test output 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-22 21:57:57 +01:00
Christoph M. Wintersteiger 93337fedeb Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-22 19:47:55 +01:00
Christoph M. Wintersteiger 31a017e99e FPA: standard function names consistency, improved error messages, bugfixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-22 19:47:50 +01:00
Ken McMillan 5454e38935 replaced check_interpolants option with interp.check 2014-10-22 10:43:04 -07:00
Ken McMillan 6e18f44d99 fixed error check in read_interpolation_problem 2014-10-22 10:42:23 -07:00
Ken McMillan d815af9f0f merge duality changes with unstable 2014-10-22 10:14:05 -07:00
Christoph M. Wintersteiger 4304012971 Java API: copyright notices 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-22 16:55:08 +01:00
Christoph M. Wintersteiger 43269795c8 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-22 16:29:46 +01:00
Christoph M. Wintersteiger d91a114b80 Java API: removed Z3_get_param_value as in other APIs. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-22 16:29:13 +01:00
Nikolaj Bjorner 65ce445b7e update Java API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-22 08:24:49 -07:00
Nuno Lopes ae6121525a Z3Py: improve readability of Z3 exceptions 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-22 13:57:07 +01:00
Nikolaj Bjorner 1059d226e4 add default statement instead of incomplete cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 13:25:19 -07:00
Nikolaj Bjorner d77d6c6648 update parameter checking for doubles, and fix error reporting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 13:24:31 -07:00
Nikolaj Bjorner f3a04734d9 add pretty printing to SMT2 from solver, add get_id to Ast objects 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 12:48:49 -07:00
Nikolaj Bjorner 3ecffaa1e5 remove unused and always failing get_param_value function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 11:12:50 -07:00
Nikolaj Bjorner 340f765983 make sure that parameters are appended such that multiple paramters are not ignored on the solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 09:35:32 -07:00
Nikolaj Bjorner 983f9abf15 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-21 09:11:53 -07:00
Nikolaj Bjorner 7f04529080 validate types of parameter values that get set globally 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 09:11:38 -07:00