match: fix test cases

kframework · Jun 10, 2020 · 6765aa7 · 6765aa7
1 parent c83380f
commit 6765aa7
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 6 deletions.
diff --git a/prover/t/unit/match-assoc-comm.k b/prover/t/unit/match-assoc-comm.k
@@ -229,20 +229,24 @@ module TEST-MATCH-ASSOC-COMM
              )
        .Declarations
 
-  rule test("match-assoc-comm", 13)
-    => assert( #error( "???" ), .MatchResults
+  rule test("match-assoc-comm", 12)
+    => assert( #matchResult( subst: W0 { Loc } |-> Y0 { Loc }
+                           , rest: .Patterns
+                           )
+             , .MatchResults
             == #match( terms:     \and(sep( pto ( Y0 { Loc } , c ( Z { Loc }))
                                           , pto ( X0 { Loc } , c ( Y0 { Loc }))
                                       )   )
-                      , pattern:   pto ( X0 { Loc } , c ( W0 { Loc }))
-                                 , pto ( W0 { Loc } , c ( Z { Loc }))
+                      , pattern:   sep ( pto ( X0 { Loc } , c ( W0 { Loc }))
+                                       , pto ( W0 { Loc } , c ( Z { Loc }))
+                                       )
                       , variables: W0 { Loc }
                       )
              )
        .Declarations
 
   // matching on mu terms with different binders
-  rule test("match-assoc-comm", 14)
+  rule test("match-assoc-comm", 13)
     => assert( #matchResult( subst: .Map , rest: .Patterns )
              , .MatchResults
             == #matchAssocComm( terms:     \mu #X0 . \and(#X0, #PHI1)

diff --git a/prover/t/unit/match-assoc.k b/prover/t/unit/match-assoc.k
@@ -124,7 +124,7 @@ module TEST-MATCH-ASSOC
   // Match multiple occurances of a variable
   rule test("match-assoc", 10)
     => symbol c ( Data ) : Data
-       assert( #matchResult( subst:    X0 |-> c( #hole )
+       assert( #matchResult( subst:    X0 { Data } |-> c( #hole )
                            , rest:     .Patterns
                            )
              , .MatchResults