From e593cac2f055761327281a326bad785d02aedd35 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Thu, 17 Mar 2011 17:42:40 +0000
Subject: [PATCH]

---
 WISHLIST | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/WISHLIST b/WISHLIST
index 375ac874a..c4e6deb64 100644
--- a/WISHLIST
+++ b/WISHLIST
@@ -4,7 +4,12 @@ Do Add here what you would love FunCheck to be able to do
 PS: support multiple top-level objects
 PS: support tuples (including natively in Z3)
 PS: implement @induct tactic, completely, not just for one arg
-PS: instantiate/unroll function bodies in a fair way, to guarantee termination
+PS: construct models for sets properly (also in interpreter)
+PS: support maps natively
+
+PS: use different levels of summaries (eg. just contract, part of contract
+that's public, then finally body) in unrollings, trying to minimize the
+branching at first
 
 Wishes granted so far
 ---------------------
@@ -16,3 +21,4 @@ PS: generate VCs for preconditions
 PS: generate VCs for pattern-matching
 PS: use 'private' accessor to indicate what's part of the interface
 PS: use a theory plugin to instantiate/unroll function bodies
+PS: instantiate/unroll function bodies in a fair way, to guarantee termination
-- 
GitLab