mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
1930 commits 23 branches 48 tags 157 MiB
Commit graph

1930 commits

This branch
This branch
All branches
Author SHA1 Message Date
Ken McMillan
a4f3afd70d added fixedpoint.conjecture_file option 2014-05-05 14:29:54 -07:00
Christoph M. Wintersteiger
581bbb58fb typo 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-05-02 18:04:32 +01:00
Christoph M. Wintersteiger
8150bd5617 OSX timeout handling bugfix 2014-05-02 17:58:17 +01:00
Christoph M. Wintersteiger
769b2b585b fixed typo 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-05-02 16:43:32 +01:00
Christoph M. Wintersteiger
fceaf97c95 Merge branch 'unstable' of https://git01.codeplex.com/z3 into bvsls 2014-04-25 22:11:34 +01:00
Christoph M. Wintersteiger
a5ce28d82a bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 22:10:53 +01:00
Christoph M. Wintersteiger
39b562da44 compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 22:03:26 +01:00
Christoph M. Wintersteiger
23dccdc7d5 compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 21:54:08 +01:00
Christoph M. Wintersteiger
c9c40877a7 compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 21:49:35 +01:00
Christoph M. Wintersteiger
4ff6a7c38d compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 18:11:30 +01:00
Christoph M. Wintersteiger
bfdea4242c removed unused file 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 18:03:35 +01:00
Christoph M. Wintersteiger
a3f20774a8 BVSLS comments 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 17:17:47 +01:00
Andreas Froehlich
3df2967be9 Cleaned up final SLS version. Enjoy! 2014-04-25 13:56:15 +01:00
Ken McMillan
f4790a183d strarting on conjecture printing in duality 2014-04-24 16:18:20 -07:00
Christoph M. Wintersteiger
fb4c07a2ea FPA refactoring in preparation for FPA support in the kernel. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-23 18:36:38 +01:00
Andreas Froehlich
9ebfb119db Moved parameters to the right file. Almost clean. 2014-04-23 14:52:18 +01:00
Nikolaj Bjorner
4d2d334999 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-04-23 14:44:03 +02:00
Nikolaj Bjorner
7d16ed9fdc fix exception class in python API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-23 14:13:01 +02:00
Ken McMillan
2755854c81 trying alternate encoding of distint 2014-04-22 16:42:35 -07:00
Ken McMillan
77f8aa9f6b fix for quantifiers in interpolants 2014-04-22 13:28:11 -07:00
Andreas Froehlich
c441bb4388 Backup before I touch early pruning ... 2014-04-22 16:10:44 +01:00
Andreas Froehlich
8346aed39c Fixed bug with VNS repick. 2014-04-22 01:07:30 +01:00
Andreas Froehlich
c1741d7941 Almost cleaned up version. 2014-04-22 00:32:45 +01:00
Andreas Froehlich
5ab65d52a6 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into bvsls 
Conflicts:
	src/tactic/sls/sls_engine.cpp
	src/tactic/sls/sls_engine.h
	src/tactic/sls/sls_evaluator.h
	src/tactic/sls/sls_tracker.h
 2014-04-21 17:05:19 +01:00
Andreas Froehlich
ef1d8f2acc Current version before integration ... 2014-04-20 16:38:49 +01:00
Ken McMillan
60ef669fbc removed distinct predicate hack 2014-04-10 17:54:49 -07:00
Ken McMillan
de81db9a3b fixed several interpolation problems 2014-04-10 17:53:17 -07:00
Ken McMillan
f7d589fc49 changed fixedpoint output format for easier parsing in Boogie 2014-04-10 17:53:00 -07:00
Christoph M. Wintersteiger
52b54f395b FPA division bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-10 19:33:34 +01:00
Christoph M. Wintersteiger
64bfbb657c .NET API documentation XML build fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-09 11:39:05 +01:00
Christoph M. Wintersteiger
1572d790cf Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-04-09 11:31:52 +01:00
Christoph M. Wintersteiger
aa006fa237 added dotnet generated files to .gitignore 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-09 11:31:44 +01:00
Christoph M. Wintersteiger
a3b89a8af3 .NET API documentation fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-09 11:24:42 +01:00
Christoph M. Wintersteiger
b6c0b8c9ff Compilation fix for FreeBSD 2014-04-07 16:09:22 +01:00
Ken McMillan
58ffffe4d4 hack to filter out Boogie axioms with large "distinct" predicates that cause legacy solver death 2014-04-06 13:01:20 -07:00
Ken McMillan
2b492f04f6 merging duality and interpolation changes 2014-04-04 15:50:59 -07:00
Ken McMillan
bdc7bfde87 duality quantifier simplification fix 2014-04-04 13:10:18 -07:00
Christoph M. Wintersteiger
dee21c6656 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-04-04 17:57:57 +01:00
Christoph M. Wintersteiger
9c052f589d C API bugfix (Stackoverflow #22864146) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-04 17:57:50 +01:00
Ken McMillan
43644fc2cb g++ pedantry 2014-04-04 01:28:09 +01:00
Ken McMillan
588aeff5c3 merged interpolation and duality changes 2014-04-03 17:11:15 -07:00
Ken McMillan
fc62be37b6 getting rid of DOS line endings 2014-04-03 17:09:11 -07:00
Ken McMillan
9a2fe83697 interpolation fix 2014-04-03 13:20:08 -07:00
Christoph M. Wintersteiger
4444eb361c bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-03 13:11:39 +01:00
Christoph M. Wintersteiger
944dfee008 .NET and Java API Bugfix (Codeplex issue 101) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-02 19:25:05 +01:00
Christoph M. Wintersteiger
7bb1469d71 removed debugging code. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-02 19:10:30 +01:00
Christoph M. Wintersteiger
a833c9ac41 Fixed bug (codeplex issue 102) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-02 17:56:55 +01:00
Ken McMillan
4671c1be41 duality fix 2014-04-01 17:50:48 -07:00
Ken McMillan
278d619521 set text default to auto to try to avoid crlf disasters 2014-04-01 17:20:37 -07:00
Ken McMillan
6c9483c70a interpolation fix and improving duality quantifier handling 2014-04-01 17:10:14 -07:00