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

1898 commits

This branch
This branch
All branches
Author SHA1 Message Date
Ken McMillan
a4584f4eaa Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-10 14:46:40 -07:00
Ken McMillan
30a4627a1e fixed problem with nullary background constants in duality 2013-06-10 14:46:15 -07:00
Nikolaj Bjorner
0210156bf0 add convex interior generalizer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-10 10:51:56 -04:00
Ken McMillan
a6d61e3404 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-07 16:17:16 -07:00
Ken McMillan
c21cd6ffa5 fixed model completion problem in duality 2013-06-07 16:16:56 -07:00
Ken McMillan
b78752ef04 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-07 11:51:33 -07:00
Ken McMillan
adb1f95e0a small fixes in duality 2013-06-07 11:51:22 -07:00
Ken McMillan
40fe1f6e99 adjusting stratified inlining in duality 2013-06-07 11:50:01 -07:00
Christoph M. Wintersteiger
455618bb2b FPA: added is_nan 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 18:34:31 +01:00
Christoph M. Wintersteiger
d7639557d2 FPA: added rewriting and fpa2bv conversion rules for new operations. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 18:03:46 +01:00
Christoph M. Wintersteiger
123d3ec3a7 New FPA operators added. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 17:55:29 +01:00
Christoph M. Wintersteiger
e5c720de29 FPA: bugfix for abs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 17:36:34 +01:00
Christoph M. Wintersteiger
724f2af8c7 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-07 17:34:38 +01:00
Leonardo de Moura
2b59f2ecc2 Fix issue https://z3.codeplex.com/workitem/37 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-06 18:29:29 -07:00
Leonardo de Moura
f4f1c63abb Fix issue https://z3.codeplex.com/workitem/38 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-06 13:20:43 -07:00
Ken McMillan
c57509d795 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-05 18:02:14 -07:00
Ken McMillan
de7a675afa a mistake 2013-06-05 18:02:07 -07:00
Ken McMillan
97a7ae1589 add profiling option 2013-06-05 18:01:05 -07:00
Ken McMillan
c3eae9bf2a working on incremental stratified inlining in duality 2013-06-05 17:02:13 -07:00
Leonardo de Moura
110fa0b7fb Fix issue http://z3.codeplex.com/workitem/45 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-05 13:50:22 -07:00
Christoph M. Wintersteiger
d301bd35a9 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-05 14:36:18 +01:00
Ken McMillan
418f148ecf working on incremental stratified inlining in duality 2013-06-04 18:22:54 -07:00
Nikolaj Bjorner
b6d9d8a601 fix bugs reported by Nuno Lopes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-04 12:55:35 -07:00
Nikolaj Bjorner
aa0d921240 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-03 11:48:21 -07:00
Nikolaj Bjorner
bd064bf5d0 enable UTVPI by default 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-03 11:46:13 -07:00
Christoph M. Wintersteiger
093fe945bc FPA: min/max/fma bugfixes + partial quantifier support 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-03 18:19:45 +01:00
Christoph M. Wintersteiger
7c32df93a4 SLS tactic: compilation fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-03 18:17:41 +01:00
Nikolaj Bjorner
56bfc06c4f fix reference count bugs in overflow/underflow APIs for bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-02 20:55:15 -07:00
Nikolaj Bjorner
d569027e36 fix reference count bugs in overflow/underflow APIs for bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-02 20:54:01 -07:00
Nikolaj Bjorner
89d8970d41 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-02 12:03:01 -07:00
Nikolaj Bjorner
ec121db5c1 addressing race condition on interrupts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-02 12:02:35 -07:00
Nikolaj Bjorner
76a269c85a clean up parity computation 
Signed-off-by: unknown <nbjorner@NIKOLAJ-ZEN.redmond.corp.microsoft.com>
 2013-06-01 17:14:18 -07:00
Ken McMillan
9890b3bb5c changing model format in duality to support boogie 2013-05-31 18:00:50 -07:00
Ken McMillan
ca38158966 fix bug in getting decision count in duality 2013-05-31 17:52:51 -07:00
Nikolaj Bjorner
c0895e5548 remove hassel table from unstable: does not compile under other plantforms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-31 17:48:19 -07:00
Leonardo de Moura
b670f0bb69 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-05-30 10:55:19 -07:00
Leonardo de Moura
37215b03bc Remove redundant register_on_timeout_proc 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-05-29 18:18:24 -07:00
Nikolaj Bjorner
60c4973c1d fix crash in proof generation in BMC 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-29 17:56:23 -07:00
Ken McMillan
dfae0c5109 output background model in duality counterexamples 2013-05-29 16:40:47 -07:00
Nuno Lopes
9a66696639 merge hassel table code from branch 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-05-29 14:35:32 -07:00
Ken McMillan
ee4b9d46f1 fix labels bug in duality 2013-05-27 19:22:47 -07:00
Ken McMillan
b27abc501e set proof mode by default to avoid crash on pop if we set it later in duality 2013-05-27 19:22:19 -07:00
Leonardo de Moura
fbbbfad564 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-05-27 17:49:29 -07:00
Leonardo de Moura
c6f4cdab0f Fix bug reported at https://z3.codeplex.com/workitem/41 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-05-27 17:49:03 -07:00
Leonardo de Moura
edb2f8554d Add new example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-05-27 17:45:56 -07:00
Nikolaj Bjorner
7c12ab4716 fix some compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-25 14:40:57 -07:00
Nikolaj Bjorner
ccf10d0abe fix crash in PDR engine when transformations don't produce output predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-25 14:38:02 -07:00
Leonardo de Moura
09945dc2cb Fix compilation error with gcc 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-05-23 08:07:19 -07:00
Ken McMillan
058c8d2083 fixing labels in duality 2013-05-22 15:42:25 -07:00
Ken McMillan
9d611997b3 fixing labels in duality 2013-05-22 15:18:50 -07:00