ada/z3
0
0
Fork 0
mirror of https://github.com/AdaCore/z3.git synced 2026-02-12 12:40:40 -08:00
Code Issues Packages Projects Releases Wiki Activity
17,444 Commits 55 Branches 6 Tags
ms-master
Commit Graph

81 Commits

Author SHA1 Message Date
Nikolaj Bjorner
f6595c161f add examples with proof replay 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-19 17:43:56 -07:00
Nikolaj Bjorner
88d10f7fe4 add example for monitoring proof logs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-19 13:37:51 -07:00
Nikolaj Bjorner
791ca02ab1 formula simplification example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-11 09:33:36 +03:00
Nikolaj Bjorner
dd46224a1d use structured proof hints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 09:37:41 -07:00
Nikolaj Bjorner
a5d588ce09 add example for #5933 2022-04-05 04:26:40 +02:00
Nikolaj Bjorner
053cb72cc2 handle return status 2022-04-04 20:19:15 +02:00
Nikolaj Bjorner
4f6811a6a2 with simplification 2022-04-03 21:10:53 -07:00
Nikolaj Bjorner
53f72d9cbe updated mini 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 15:44:49 -08:00
Matteo Nicoli
cbdd7b0696 three smt2 examples added and one python example updated (#5690) 2021-12-01 16:21:12 -08:00
rainoftime
b5deba8426 add EFSMT solving example (#5654) 
Co-authored-by: rainoftime <rainoftime@gmail.com>
 2021-11-09 11:05:10 -08:00
Nikolaj Bjorner
a1b036a4fa Update README.md 2021-04-25 17:02:34 -07:00
Nikolaj Bjorner
3ff5d4226a Update README.md 2021-04-25 16:59:53 -07:00
Tias Guns
a52b485d9c marco: immediately shrink to core if not subset (#5203) 
Small improvement, found while translating it in another system
 2021-04-20 12:29:52 -07:00
Nikolaj Bjorner
7fab0f5923 updated experiment 2021-03-26 14:58:23 -07:00
Nikolaj Bjorner
7eceeff349 move branch of unit variable 2021-03-08 10:09:04 -08:00
Nikolaj Bjorner
3c26a965e1 updated script, add comment to mk_eq_empty 2021-03-07 06:59:58 -08:00
Nikolaj Bjorner
8de96009cd na 2021-03-06 12:36:19 -08:00
Nikolaj Bjorner
8d54e83567 updated hitting set sample 2021-03-06 10:18:52 -08:00
Nikolaj Bjorner
022a1fd3dd fix #5080 assertion is violated on legal input, add an example 2021-03-05 15:01:39 -08:00
Nuno Lopes
1bb9a02160 travis timeouts 2021-02-21 13:13:19 +00:00
Matteo Nicoli
785fab74f4 Create bubble_sort.py (#4976) 2021-01-26 09:42:17 -08:00
Andrew V. Jones
bb9cd5dd49 Ensure that the 'OUTPUT' locations in CMake for Python examples is accurate (#4499) 
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
 2020-06-04 15:04:01 -07:00
Bruce Mitchener
0edd587e5a Fix typos in examples. 2019-08-14 22:00:50 -07:00
Nikolaj Bjorner
807095a344 fix #2375 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-03 10:04:00 +07:00
Nikolaj Bjorner
e5dffeace4 fix #2365 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-30 08:40:41 +03:00