mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
1951 commits 49 branches 53 tags 182 MiB
Commit graph

1951 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
4e8c0c1418 compilation fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:14:19 +00:00
Christoph M. Wintersteiger
ff7af2680d compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:14:17 +00:00
Christoph M. Wintersteiger
beef8198a4 removed dependency of bvsls on goal_refs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:14:16 +00:00
Christoph M. Wintersteiger
cf1a600fb9 bugfix 2015-01-12 17:14:15 +00:00
Christoph M. Wintersteiger
e9482a1447 disabled old code 2015-01-12 17:14:13 +00:00
Christoph M. Wintersteiger
dfd2566e25 removed dependency of bvsls on goal_refs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:14:13 +00:00
Andreas Froehlich
1e55b3bfb5 uct forget and minisat restarts added 2015-01-12 17:14:12 +00:00
Christoph M. Wintersteiger
a6227d5446 SLS refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:13:59 +00:00
Christoph M. Wintersteiger
b1eeb9adf4 SLS refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:13:59 +00:00
Andreas Froehlich
aa6f8a4b8a Current version for relocating. 2015-01-12 17:13:42 +00:00
Christoph M. Wintersteiger
e33e637ad8 removed tabs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:13:12 +00:00
Andreas Froehlich
e310ab5cd7 plenty of new stuff 2015-01-12 17:13:12 +00:00
Andreas Froehlich
b002697e03 some extensions/modifications. versions added. 2015-01-12 17:13:11 +00:00
Andreas Froehlich
40014d019c sls tactic default 2015-01-12 17:13:10 +00:00
Christoph M. Wintersteiger
376614a782 Java API: slight overhaul in preparation for the FP additions 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-03 15:09:52 +00:00
Christoph M. Wintersteiger
8e7278f02c Java API: Removed unnecessary imports 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-02 18:10:47 +00:00
Christoph M. Wintersteiger
9dd4d7b011 Python API bugfix. Thanks to Tom Ball for reporting this one. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-21 20:43:26 +00:00
Nikolaj Bjorner
18c3c1d9d6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-12-16 11:21:24 -08:00
Nikolaj Bjorner
f4d256ef30 fix issue 153: assert rem/mod axiom no matter what is status of second argument 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-16 11:20:34 -08:00
Christoph M. Wintersteiger
d53fdb2848 typo 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-16 15:36:31 +00:00
Christoph M. Wintersteiger
1244d5a22e Python API: Added BVRedAnd, BVRedOr 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-16 15:28:52 +00:00
Ken McMillan
882dbfc706 merge 2014-12-08 16:16:52 -08:00
Ken McMillan
8181b15a1b attempted interp fixes 2014-12-08 15:46:55 -08:00
Nikolaj Bjorner
45755bbd14 fix context sensitivity. Codeplex issue 148, thanks to clockish 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-03 08:55:14 +09:00
Christoph M. Wintersteiger
61c59fb4bf Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-12-02 14:35:29 +00:00
Christoph M. Wintersteiger
c88b2f6b5e .NET API: Added build instructions for .NET 3.5 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-02 14:35:15 +00:00
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
Ken McMillan
a6f58bdd17 fixes and performance improvements for interp and duality 2014-10-30 17:22:34 -07: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