!!! Manual stratergy for avl-implies-bst

kframework · Feb 11, 2020 · 9394d72 · 9394d72
1 parent 81bd89a
commit 9394d72
Showing 1 changed file with 7 additions and 8 deletions.
diff --git a/prover/t/avl-implies-bst.kore b/prover/t/avl-implies-bst.kore
@@ -18,11 +18,10 @@ claim \implies( \and( avl( H { ArrayIntInt }
                          )
                     )
               )
-strategy search-fol(bound: 3)
-//strategy simplify . kt . simplify
-//       . ( (right-unfold-Nth(0,0) . simplify . instantiate-existentials . smt )
-//         | (right-unfold-Nth(0,1) . simplify . instantiate-existentials . smt )
-//         | (instantiate-existentials . smt )
-//         | (right-unfold-Nth(0,2) . simplify . instantiate-existentials . smt )
-//         | noop
-//         )
+// strategy search-fol(bound: 3)
+strategy normalize . simplify . kt . normalize . simplify
+       . ( (right-unfold-Nth(0,0) . normalize . simplify . instantiate-existentials . smt )
+         | (right-unfold-Nth(0,1) . normalize . simplify . instantiate-existentials . smt )
+         | (instantiate-existentials . smt )
+         | (right-unfold-Nth(0,2) . normalize . simplify . instantiate-existentials . smt )
+         )