mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity
3750 commits 24 branches 48 tags 158 MiB
Commit graph

127 commits

Author SHA1 Message Date
Ken McMillan
3d2ef8bb4a fix for issue #109 2015-05-27 16:05:40 -07:00
Ken McMillan
e438143abc fix for github issue #105 2015-05-22 11:02:26 -07:00
Ken McMillan
caa616f11b fix for github issue 83 2015-05-20 15:37:51 -07:00
Ken McMillan
ccc1f02216 fix for github issue 54 2015-05-19 18:47:13 -07:00
Christoph M. Wintersteiger
32fb679066 tabs 2015-05-19 11:01:15 +01:00
Nikolaj Bjorner
9377779e58 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-30 10:40:03 -07:00
Ken McMillan
5f37b1d32f fixed interp api bug (github issue #47) 2015-04-20 12:30:15 -07:00
Ken McMillan
af444beb2e re-indenting interp and duality 2015-04-15 12:22:50 -07:00
Nikolaj Bjorner
3ba2e712b2 merge with unstable branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-12 15:54:52 -07:00
Ken McMillan
d42e3ce651 possible header problem for std::less 2015-04-02 13:10:23 -07:00
Nikolaj Bjorner
52619b9dbb pull unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 14:57:11 -07:00
Ken McMillan
be709802cd merging interpolation fix (issue 182) 2015-03-20 17:46:01 -07:00
Ken McMillan
47d33452c6 interpolation fix (issue 182) 2015-03-20 17:39:45 -07:00
nikolajbjorner
a96a9a076d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-02-19 19:10:21 -08:00
nikolajbjorner
aa40316268 rewrite terminology for policheck 
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
 2015-02-19 19:09:12 -08:00
Ken McMillan
185f9325a6 fixed interpolation bug 2015-02-19 12:25:06 -08:00
Nikolaj Bjorner
c61e9f27db local changes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-22 09:27:33 -08:00
Nikolaj Bjorner
08cb8b8de8 address divergence in the case of shared theory symbols. Codeplex issue 147, thanks to George Karpenkov 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-09 16:04:25 +01: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
Christoph M. Wintersteiger
005bb82a17 eliminated unused variables 2014-11-07 16:04:02 +00:00
Ken McMillan
a6f58bdd17 fixes and performance improvements for interp and duality 2014-10-30 17:22:34 -07: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
a6bee82ef8 Interpolation API: fixed some memory leaks 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-23 17:10:31 +01:00
Ken McMillan
5454e38935 replaced check_interpolants option with interp.check 2014-10-22 10:43:04 -07:00
Nikolaj Bjorner
e6725b2344 merge unstable into opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-26 12:12:24 -07:00
Ken McMillan
ab13987884 working on python interp 2014-08-06 11:16:24 -07:00
Ken McMillan
7bf87e76ea fix for tree interpolation 2014-08-05 11:11:43 -07:00
Nikolaj Bjorner
960e8ea1d5 working on hitting sets 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-08 14:12:54 +01:00
Ken McMillan
97c5d09de1 turn off a windows warning 2014-05-21 16:56:18 -07:00
Ken McMillan
06b79cd9ea trying to prevent quantifier in interp (leq2eq rule) 2014-05-21 13:30:54 -07:00
Ken McMillan
95146483ea add round-off to farkas resconstruction in interp 2014-05-13 18:15:51 -07:00
Ken McMillan
c9e9b30af6 interp handle mystery arith lemmas 2014-05-13 17:28:22 -07:00
Ken McMillan
669fded98a fix for possible problem in Farkas proofs in interp 2014-05-13 14:59:09 -07:00
Ken McMillan
aa35f988fc fix for bad coefficient in AssignBounds 2014-05-13 14:58:32 -07:00
Ken McMillan
2a887a7608 interp localization hack 2014-05-09 13:08:39 -07:00
Nikolaj Bjorner
9c1f85e564 addressing compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-09 11:03:11 -07:00
Christoph M. Wintersteiger
c3b7c738f8 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into opt 
Conflicts:
	scripts/mk_project.py
	src/duality/duality.h
	src/duality/duality_solver.cpp
	src/duality/duality_wrapper.h
	src/interp/iz3hash.h

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 22:18:41 +01:00
Ken McMillan
77f8aa9f6b fix for quantifiers in interpolants 2014-04-22 13:28:11 -07:00
Ken McMillan
de81db9a3b fixed several interpolation problems 2014-04-10 17:53:17 -07:00
Ken McMillan
43644fc2cb g++ pedantry 2014-04-04 01:28:09 +01: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
Nikolaj Bjorner
1db7e0a149 fix compiler warnings reported by Robert White 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-02 15:54:28 +02:00
Ken McMillan
6c9483c70a interpolation fix and improving duality quantifier handling 2014-04-01 17:10:14 -07:00
Nikolaj Bjorner
9916439913 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2014-03-28 08:35:02 -07:00
Nikolaj Bjorner
a6d7d23bb5 fix compilation warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-28 08:34:54 -07:00
Nikolaj Bjorner
ac7fffa9cb fix bug exposed by example by Robert White 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-28 08:34:31 -07:00
Ken McMillan
732035bf63 merge interp/duality changes with unstable 2014-03-26 14:48:04 -07:00