From 71bcbeb4ce808f463d86b7a877e3e550e839fb17 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 22:52:14 -0700 Subject: Add a small test from the IronClad notebook --- ...ix-an-issue-listed-in-the-ironclad-notebook.dfy | 23 ++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy (limited to 'Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy') diff --git a/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy b/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy new file mode 100644 index 00000000..09032453 --- /dev/null +++ b/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy @@ -0,0 +1,23 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This example was listed in IronClad's notebook as one place were z3 picked +// much too liberal triggers. THe Boogie code for this is shown below: +// +// forall k#2: Seq Box :: $Is(k#2, TSeq(TInt)) && $IsAlloc(k#2, TSeq(TInt), $Heap) +// ==> Seq#Equal(_module.__default.HashtableLookup($Heap, h1#0, k#2), +// _module.__default.HashtableLookup($Heap, h2#0, k#2)) +// +// and z3 would pick $Is(k#2, TSeq(TInt)) or $IsAlloc(k#2, TSeq(TInt), $Heap) as +// triggers. + +type Key = seq +type Value = seq + +type Hashtable = map +function HashtableLookup(h: Hashtable, k: Key): Value + +lemma HashtableAgreement(h1:Hashtable, h2:Hashtable, k:Key) + requires forall k :: HashtableLookup(h1,k) == HashtableLookup(h2,k) { + assert true || (k in h1) == (k in h2); +} -- cgit v1.2.3