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

1090 commits

This branch
This branch
All branches
Author SHA1 Message Date
Ken McMillan 4ce39087db something cl was complaining about 2013-09-15 14:00:45 -07:00
Ken McMillan 12533ad145 Merge /home/mcmillan/projects/z3_interp into interp 2013-09-15 13:40:39 -07:00
Ken McMillan 6091cb1825 fix lemma counting and nix NEW_EXTRACT_TH_LEMMA 2013-09-15 13:40:06 -07:00
Ken McMillan 2c9c5ba1f0 still working on interpolation of full z3 proofs 2013-09-15 13:33:20 -07:00
Ken McMillan 07bb534d65 some duality fixes 2013-08-16 18:38:24 -07:00
Ken McMillan 41f77ab57c duality abort hack and debugging hacks 2013-06-27 17:29:12 -07:00
Ken McMillan d8b31773b8 some debugging stuff 2013-06-27 17:27:36 -07:00
Ken McMillan ea127c8ab9 some confusion about proof generation 2013-06-27 12:24:18 -07:00
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