runtimeverification · rv-jenkins · Sep 14, 2022 · Aug 30, 2022 · Sep 7, 2022 · Sep 7, 2022
diff --git a/k-distribution/tests/regression-new/concrete-function-cache/a2-spec.k.out b/k-distribution/tests/regression-new/concrete-function-cache/a2-spec.k.out
@@ -1,3 +1,4 @@
 <k>
   end ( bar1 ( V0 ) )
 </k>
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/concrete-function/a1-spec.k.out b/k-distribution/tests/regression-new/concrete-function/a1-spec.k.out
@@ -1,3 +1,4 @@
 <k>
   end ( bar1 ( V0 ) )
 </k>
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/issue-2142-markConcrete/test-spec.k.out b/k-distribution/tests/regression-new/issue-2142-markConcrete/test-spec.k.out
@@ -7,3 +7,4 @@
   <k>
     doneLemma ( keccak ( _Gen0 ) ) ~> _DotVar1 ~> .
   </k>
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/kprove-error-status/Makefile b/k-distribution/tests/regression-new/kprove-error-status/Makefile
@@ -0,0 +1,9 @@
+DEF=verif
+EXT=verif
+TESTDIR=.
+KOMPILE_BACKEND=haskell
+
+include ../../../include/kframework/ktest.mak
+
+KPROVE_OR_LEGACY=$(KPROVE)
+CONSIDER_PROVER_ERRORS=2>&1 | sed 's/\(kore-exec: \)\[[0-9]\+\]/\1/g'
diff --git a/k-distribution/tests/regression-new/kprove-error-status/crash-spec.k b/k-distribution/tests/regression-new/kprove-error-status/crash-spec.k
@@ -0,0 +1,9 @@
+// Copyright (c) 2019 K Team. All Rights Reserved.
+
+module CRASH-SPEC
+    imports VERIF
+
+    claim <k> doIt(foo) => doIt(0) ... </k>
+    claim <k> crash(foo) => doIt(0) ... </k>
+
+endmodule
diff --git a/k-distribution/tests/regression-new/kprove-error-status/crash-spec.k.out b/k-distribution/tests/regression-new/kprove-error-status/crash-spec.k.out
@@ -0,0 +1,15 @@
+kore-exec:  Error (ErrorException):
+    Error: missing hook
+    Symbol
+        Lblcrash'LParUndsRParUnds'VERIF-SYNTAX'Unds'Pgm'Unds'Int{}
+    declared with attribute
+        hook{}("KREFLECTION.printKORE")
+    We don't recognize that hook and it was not given any rules.
+    Please open a feature request at
+        https://github.com/runtimeverification/haskell-backend/issues
+    and include the text of this message.
+    Workaround: Give rules for Lblcrash'LParUndsRParUnds'VERIF-SYNTAX'Unds'Pgm'Unds'Int{}
+    CallStack (from HasCallStack):
+      error, called at src/Kore/Rewrite/Function/Evaluator.hs:274:6 in kore-0.60.0.0-C6NIGnCldg2CHYuzj5V8fi:Kore.Rewrite.Function.Evaluator
+Created bug report: kore-exec.tar.gz
+[Error] Critical: Haskell Backend execution failed with code 1 and produced no output.
diff --git a/k-distribution/tests/regression-new/kprove-error-status/stuck-claim-spec.k b/k-distribution/tests/regression-new/kprove-error-status/stuck-claim-spec.k
@@ -0,0 +1,15 @@
+module VERIFICATION
+  imports VERIF
+endmodule
+
+module STUCK-CLAIM-SPEC
+  import VERIFICATION
+
+  claim  <k> addCounter(N:Int) => 1 ...</k>
+         <counter> C:Int => ?_ </counter>
+         <sum> S:Int => ?S:Int </sum>
+    requires
+      N >=Int 0
+    ensures
+      ?S ==Int S +Int N *Int C +Int (N -Int 1) *Int N /Int 2
+endmodule
diff --git a/k-distribution/tests/regression-new/kprove-error-status/stuck-claim-spec.k.out b/k-distribution/tests/regression-new/kprove-error-status/stuck-claim-spec.k.out
@@ -0,0 +1,65 @@
+kore-exec:  Warning (WarnStuckClaimState):
+    (InfoReachability) while checking the implication:
+    The configuration's term doesn't unify with the destination's term and the configuration cannot be rewritten further. Location: stuck-claim-spec.k:8:10-14:61
+kore-exec:  Warning (WarnUnexploredBranches):
+    5 branches were still unexplored when the action failed.
+  #Not ( #Exists _DotVar2 . #Exists I . {
+      _DotVar1
+    #Equals
+      doIt ( I ) ~> _DotVar2 ~> .
+    }
+  #And
+    {
+      true
+    #Equals
+      I >Int 0
+    } )
+#And
+  #Not ( #Exists _DotVar2 . #Exists N . {
+      _DotVar1
+    #Equals
+      addCounter ( N ) ~> _DotVar2 ~> .
+    }
+  #And
+    {
+      true
+    #Equals
+      N >=Int 0
+    } )
+#And
+  #Not ( #Exists _DotVar2 . #Exists Times . {
+      _DotVar1
+    #Equals
+      addCounter ( Times ) ~> _DotVar2 ~> .
+    }
+  #And
+    {
+      true
+    #Equals
+      Times >Int 0
+    } )
+#And
+  #Not ( #Exists _DotVar2 . {
+    _DotVar1
+  #Equals
+    addCounter ( 0 ) ~> _DotVar2 ~> .
+  } )
+#And
+  <generatedTop>
+    <k>
+      _DotVar1
+    </k>
+    <counter>
+      C
+    </counter>
+    <sum>
+      S
+    </sum>
+  </generatedTop>
+#And
+  {
+    N
+  #Equals
+    0
+  }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/kprove-error-status/verif.k b/k-distribution/tests/regression-new/kprove-error-status/verif.k
@@ -0,0 +1,28 @@
+// Copyright (c) 2019 K Team. All Rights Reserved.
+
+module VERIF-SYNTAX
+    imports INT
+
+    syntax Int ::= "foo" [macro]
+    rule foo => 3
+
+    syntax Pgm ::= doIt ( Int )
+    syntax Pgm ::= addCounter ( Int )
+    syntax Pgm ::= crash ( Int ) [function,hook(KREFLECTION.printKORE)]
+endmodule
+
+module VERIF
+    imports VERIF-SYNTAX
+    imports BYTES
+
+    configuration <k> $PGM:Pgm </k> <counter> 1 </counter> <sum> 0 </sum>
+
+    rule <k> addCounter(0) => . ... </k>
+    rule  <k> addCounter(Times:Int => Times -Int 1) ...</k>
+          <counter> C:Int => C +Int 1 </counter>
+          <sum> S:Int => S +Int C </sum>
+      requires Times >Int 0
+
+    rule <k> doIt(I => I -Int 1) ... </k> requires I >Int 0
+
+endmodule
diff --git a/k-distribution/tests/regression-new/kprove-error-status/verif.k.out b/k-distribution/tests/regression-new/kprove-error-status/verif.k.out
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-1-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-1-spec.k.out
@@ -1,3 +1,4 @@
 <k>
   assignmentResult ( x |-> 3 ) ~> .
 </k>
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-10-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-10-spec.k.out
@@ -20,3 +20,4 @@
   #Equals
     X:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-11-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-11-spec.k.out
@@ -33,3 +33,4 @@
   #Equals
     Z:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-12-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-12-spec.k.out
@@ -14,3 +14,4 @@
   #Equals
     X:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-13-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-13-spec.k.out
@@ -14,3 +14,4 @@
   #Equals
     Z:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-14-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-14-spec.k.out
@@ -26,3 +26,4 @@
   #Equals
     X:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-15-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-15-spec.k.out
@@ -38,3 +38,4 @@
   #Equals
     Z:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-16-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-16-spec.k.out
@@ -40,3 +40,4 @@
   #Equals
     Z:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-17-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-17-spec.k.out
@@ -8,3 +8,4 @@
   #Equals
     Z:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-19-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-19-spec.k.out
@@ -8,3 +8,4 @@
   #Equals
     Z:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-2-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-2-spec.k.out
@@ -8,3 +8,4 @@
   #Equals
     X:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-20-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-20-spec.k.out
@@ -14,3 +14,4 @@
   #Equals
     Y:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-21-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-21-spec.k.out
@@ -8,3 +8,4 @@
   #Equals
     Z:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-22-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-22-spec.k.out
@@ -14,3 +14,4 @@
   #Equals
     X:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-23-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-23-spec.k.out
@@ -8,3 +8,4 @@
   #Equals
     X:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-24-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-24-spec.k.out
@@ -14,3 +14,4 @@
   #Equals
     X:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-25-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-25-spec.k.out
@@ -20,3 +20,4 @@
   #Equals
     X:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-26-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-26-spec.k.out
@@ -3,3 +3,4 @@
   1 |-> 4
   X:MyId |-> 3 ) ~> .
 </k>
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-27-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-27-spec.k.out
@@ -1,3 +1,4 @@
 <k>
   assignmentResult ( X:MyId |-> 3 ) ~> .
 </k>
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-28-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-28-spec.k.out
@@ -8,3 +8,4 @@
     assignmentResult ( ( X:MyId |-> 3 ) [ x <- 5 ]
     y |-> 4 ) ~> .
   </k>
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-29-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-29-spec.k.out
@@ -21,3 +21,4 @@
   #Equals
     Y:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-3-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-3-spec.k.out
@@ -14,3 +14,4 @@
   #Equals
     X:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-30-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-30-spec.k.out
@@ -21,3 +21,4 @@
   #Equals
     foo ( Y ) in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-31-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-31-spec.k.out
@@ -21,3 +21,4 @@
   #Equals
     foo ( Y ) in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-4-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-4-spec.k.out
@@ -20,3 +20,4 @@
   #Equals
     Y:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-5-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-5-spec.k.out
@@ -21,3 +21,4 @@
   #Equals
     Y:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-6-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-6-spec.k.out
@@ -8,3 +8,4 @@
   #Equals
     Y:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-7-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-7-spec.k.out
@@ -14,3 +14,4 @@
   #Equals
     Z:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-8-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-8-spec.k.out
@@ -14,3 +14,4 @@
   #Equals
     Z:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-9-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-9-spec.k.out
@@ -20,3 +20,4 @@
   #Equals
     X:MyId in_keys ( MAP )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-1-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-1-spec.k.out
@@ -1,3 +1,4 @@
 <k>
   inkeysResult ( false ) ~> .
 </k>
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-10-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-10-spec.k.out
@@ -1,3 +1,4 @@
 <k>
   inkeysResult ( true ) ~> .
 </k>
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-11-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-11-spec.k.out
@@ -1,3 +1,4 @@
 <k>
   inkeysResult ( Y:MyId in_keys ( M [ X:MyId <- 0 ] ) ) ~> .
 </k>
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-12-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-12-spec.k.out
@@ -7,3 +7,4 @@
   #Equals
     Y:MyId in_keys ( M )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-13-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-13-spec.k.out
@@ -7,3 +7,4 @@
   #Equals
     Y:MyId in_keys ( M )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-14-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-14-spec.k.out
@@ -1,3 +1,4 @@
 <k>
   inkeysResult ( true ) ~> .
 </k>
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-15-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-15-spec.k.out
@@ -1,3 +1,4 @@
 <k>
   inkeysResult ( Y:MyId in_keys ( M [ Z:MyId <- 1 ] [ X:MyId <- 0 ] ) ) ~> .
 </k>
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-16-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-16-spec.k.out
@@ -7,3 +7,4 @@
   #Equals
     Y:MyId in_keys ( M )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-17-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-17-spec.k.out
@@ -7,3 +7,4 @@
   #Equals
     Y:MyId in_keys ( M )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-2-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-2-spec.k.out
@@ -7,3 +7,4 @@
   #Equals
     X:MyId in_keys ( M )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-3-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-3-spec.k.out
@@ -8,3 +8,4 @@
   #Equals
     X:MyId in_keys ( M )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-4-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-4-spec.k.out
@@ -14,3 +14,4 @@
   #Equals
     Y:MyId in_keys ( M )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-5-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-5-spec.k.out
@@ -14,3 +14,4 @@
   #Equals
     Y:MyId in_keys ( M )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-6-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-6-spec.k.out
@@ -19,3 +19,4 @@
   #Equals
     Z:MyId in_keys ( M )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-7-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-7-spec.k.out
@@ -21,3 +21,4 @@
   #Equals
     Z:MyId in_keys ( M )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-8-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-8-spec.k.out
@@ -27,3 +27,4 @@
   #Equals
     Y:MyId in_keys ( M )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-9-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/inkeys-9-spec.k.out
@@ -27,3 +27,4 @@
   #Equals
     Z:MyId in_keys ( M )
   }
+[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
-Original file line number
+Diff line change
@@ Expand Up / @@ -7,3 +7,4 @@ @@
       <k>
         doneLemma ( keccak ( _Gen0 ) ) ~> _DotVar1 ~> .
       </k>
+    [Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.