Weakened a sequence axiom trigger to resolve #601

viperproject · Mar 8, 2022 · 4ca96a4 · 4ca96a4
1 parent cd20cf0
commit 4ca96a4
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/main/resources/dafny_axioms/sequences.vpr b/src/main/resources/dafny_axioms/sequences.vpr
@@ -53,7 +53,9 @@ domain $Seq[E] {
   }
 
   axiom seq_index_over_singleton {
-    forall e: E :: {Seq_index(Seq_singleton(e), 0)}
+    forall e: E ::
+        // {Seq_index(Seq_singleton(e), 0)}
+        {Seq_singleton(e)} // [2022-03-08 Malte] Weaker trigger to resolve Silicon issue #601
       Seq_index(Seq_singleton(e), 0) == e
   }