Update dependency: haskell-backend/src/main/native/haskell-backend

[rv-jenkins]

No description provided.

[ehildenb]

With this patch:

commit 51a5505a1d7c811aaa413611faa9d08009c6d344 (_update-deps_runtimeverification_haskell-backend)
Author: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date:   Wed Nov 30 20:33:50 2022 +0000

    set-symbolic-tests/inset-11-spec.k: update expected output

diff --git a/k-distribution/tests/regression-new/set-symbolic-tests/inset-11-spec.k.out b/k-distribution/tests/regression-new/set-symbolic-tests/inset-11-spec.k.out
index 1d23c8966c..2d6852aa97 100644
--- a/k-distribution/tests/regression-new/set-symbolic-tests/inset-11-spec.k.out
+++ b/k-distribution/tests/regression-new/set-symbolic-tests/inset-11-spec.k.out
@@ -3,6 +3,13 @@
     SetItem ( X:MyId )
     SetItem ( Z:MyId ) ) ~> .
   </k>
+#And
+  {
+    false
+  #Equals
+    X:MyId in SET
+    SetItem ( Z:MyId )
+  }
 #And
   {
     false
@@ -16,4 +23,10 @@
     Z:MyId in SET
     SetItem ( X:MyId )
   }
+#And
+  {
+    false
+  #Equals
+    Z:MyId in SET
+  }
 [Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.

Then the tests pass.

In particular, the test looks like this:

// Copyright (c) 2022 K Team. All Rights Reserved.
// generated by gen-tests.sh

requires "set-tests.k"

module INSET-11-SPEC
    imports SET-TESTS

    claim <k> inSet ( Y:MyId in ( SetItem(Z:MyId) SET:Set SetItem(X:MyId) ) ) => . </k>

endmodule

And the original output looks like this:

  <k>
    inSetResult ( Y:MyId in SET
    SetItem ( X:MyId )
    SetItem ( Z:MyId ) ) ~> .
  </k>
#And
  { 
    false
  #Equals
    X:MyId in SET
  }
#And
  {
    false
  #Equals
    Z:MyId in SET
    SetItem ( X:MyId )
  }
[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.

But the new output looks like this:

  <k>
    inSetResult ( Y:MyId in SET
    SetItem ( X:MyId )
    SetItem ( Z:MyId ) ) ~> .
  </k>
#And
  { 
    false
  #Equals
    X:MyId in SET
    SetItem ( Z:MyId ) 
  }
#And
  {
    false
  #Equals
    X:MyId in SET 
  } 
#And 
  { 
    false 
  #Equals 
    Z:MyId in SET
    SetItem ( X:MyId )
  } 
#And 
  { 
    false 
  #Equals 
    Z:MyId in SET 
  }
[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.

So, it's added the extra conditions { false #Equals X in SET SetItem(Z) } and { false #Equals Z in SET } are added. These are both valid conditions triggered by assuming #Ceil of the LHS of the proof obligation, but I'm wondering why we didn't have them before?

We need to find out why the change in test output is needed.

[ehildenb]

The first commit in the backend which causes this change is this one: runtimeverification/haskell-backend#3338