mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
1082 commits 49 branches 53 tags 182 MiB
Commit graph

1082 commits

This branch
This branch
All branches
Author SHA1 Message Date
Ken McMillan
0eb46eef00 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-27 11:30:09 -07:00
Ken McMillan
4d939c07a3 fixed bug in range computation 2013-06-27 11:28:38 -07:00
Ken McMillan
5b87fb4cc3 merge of Leo's changes 2013-06-25 12:34:37 -07:00
Ken McMillan
dfbccf6cc3 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-25 12:25:51 -07:00
Ken McMillan
7cc6ff0a4c changed timeout behavior in duality 2013-06-25 12:25:41 -07:00
Leonardo de Moura
efb6b2453e Move AssemblyInfo.cs AssemblyInfo. Update mk_util.py to generate AssemblyInfo.cs instead of modifying it. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-24 15:37:49 -07:00
Ken McMillan
1578a7fd95 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-18 12:29:58 -07:00
Ken McMillan
0f13ec6e42 adding timeout to duality 2013-06-18 12:28:20 -07:00
Ken McMillan
c448b2a430 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-17 18:07:23 -07:00
Ken McMillan
64acd9cac0 fixed some bugs with quantifiers in rule bodies 2013-06-17 18:04:23 -07:00
Ken McMillan
7a85c8951e Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-14 16:46:41 -07:00
Ken McMillan
a78564145b hooked up array.weak and array.extension params 2013-06-14 16:46:13 -07:00
Ken McMillan
782ffc32e8 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-14 16:34:41 -07:00
Ken McMillan
886128c989 hooked up array.weak and array.extension params 2013-06-14 16:33:51 -07:00
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
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
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
Ken McMillan
418f148ecf working on incremental stratified inlining in duality 2013-06-04 18:22:54 -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
Ken McMillan
dfae0c5109 output background model in duality counterexamples 2013-05-29 16:40:47 -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
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
Ken McMillan
193e255387 Merge /home/mcmillan/pc/Code/z3_interp into interp 2013-05-22 13:31:24 -07:00
Ken McMillan
7905f48e88 status reporting issue 2013-05-22 13:23:37 -07:00
Ken McMillan
65fbef4133 fix for compiler weirdness 2013-05-10 12:16:24 -07:00
Ken McMillan
477754c386 fixed bug in label output in duality 2013-05-09 14:24:22 -07:00
Ken McMillan
dc793907a5 added rule names to duality output 2013-05-09 13:31:17 -07:00
Ken McMillan
b935e1e71a still adding labels to duality 2013-05-07 11:04:10 -07:00
Ken McMillan
389c2018df working on duality 2013-05-03 17:30:07 -07:00
Ken McMillan
2f8b7bfa18 adding labels to duality 2013-05-03 17:29:13 -07:00
Ken McMillan
e939dd2bc5 still integrating duality 2013-04-30 13:07:49 -07:00
Ken McMillan
feb5360999 integrating duality 2013-04-28 16:29:55 -07:00
Ken McMillan
8488ca24d2 first commit of duality 2013-04-20 18:18:45 -07:00
Ken McMillan
71275652a7 added simp of interpolants before print 2013-04-15 14:37:08 -07:00
Ken McMillan
6495d7b88c fixed so produce-interpolants option is not needed for compute-interpolant 2013-04-15 12:22:04 -07:00
Ken McMillan
e651f45bc0 added sequences to get-interpolant and compute-interpolant 2013-04-09 15:52:30 -07:00
Ken McMillan
bbe036bc03 adding build instructions 2013-03-28 11:38:11 -07:00
U-REDMOND\kenmcmil
7a0d49cb32 porting to windows 2013-03-28 11:18:20 -07:00
U-REDMOND\kenmcmil
28266786f3 porting to windows 2013-03-27 12:17:52 -07:00