Merge remote-tracking branch 'origin/develop'

runtimeverification · Nov 24, 2023 · e8041f4 · e8041f4
2 parents 41dfa24 + 7aa109b
commit e8041f4
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 13 deletions.
diff --git a/deps/hs-backend-booster_release b/deps/hs-backend-booster_release
@@ -1 +1 @@
-ac35589bb31831b346e143bfa98c51e670237b8e
+1b22ad45abf6209da1ec4c3d7bb65e4553072e1c
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -1,9 +1,9 @@
 {
   description = "K Framework";
   inputs = {
-    haskell-backend.url = "github:runtimeverification/haskell-backend/eebe4e9fd9dd6c606b37a384dbbfecca85943a38";
+    haskell-backend.url = "github:runtimeverification/haskell-backend/2f90bbf6a7a970fe0b8fc4c8a5c1ec3fd8aee4f1";
     booster-backend = {
-      url = "github:runtimeverification/hs-backend-booster/ac35589bb31831b346e143bfa98c51e670237b8e";
+      url = "github:runtimeverification/hs-backend-booster/1b22ad45abf6209da1ec4c3d7bb65e4553072e1c";
       inputs.nixpkgs.follows = "haskell-backend/nixpkgs";
       inputs.haskell-backend.follows = "haskell-backend";
       inputs.stacklock2nix.follows = "haskell-backend/stacklock2nix";

diff --git a/haskell-backend/src/main/native/haskell-backend b/haskell-backend/src/main/native/haskell-backend
diff --git a/hs-backend-booster/src/main/native/hs-backend-booster b/hs-backend-booster/src/main/native/hs-backend-booster
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		ac35589bb31831b346e143bfa98c51e670237b8e
		1b22ad45abf6209da1ec4c3d7bb65e4553072e1c
+17 −7		kore/src/Kore/JsonRpc.hs
+2 −22		kore/src/Kore/Log/DecidePredicateUnknown.hs
+6 −3		kore/src/Kore/Rewrite/SMT/Lemma.hs
+16 −0		kore/src/SMT.hs
+90 −71		scripts/generate-regression-tests.sh
+23,713 −12,316		test/regression-evm/test-dsvalue-peek-pass-rough-definition.kore
+6 −6		test/regression-evm/test-dsvalue-peek-pass-rough-spec.kore
+5 −2		test/regression-evm/test-dsvalue-peek-pass-rough.sh
+23,713 −12,316		test/regression-evm/test-flipper-addu48u48-fail-rough-definition.kore
+7 −7		test/regression-evm/test-flipper-addu48u48-fail-rough-spec.kore
+5 −2		test/regression-evm/test-flipper-addu48u48-fail-rough.sh
+23,583 −12,019		test/regression-evm/test-functional-definition.kore
+134 −111		test/regression-evm/test-functional-spec.kore
+5 −2		test/regression-evm/test-functional.sh
+23,394 −11,854		test/regression-evm/test-lemmas-definition.kore
+1,293 −721		test/regression-evm/test-lemmas-spec.kore
+5 −2		test/regression-evm/test-lemmas.sh
+23,580 −12,016		test/regression-evm/test-storagevar03-definition.kore
+6 −6		test/regression-evm/test-storagevar03-spec.kore
+5 −2		test/regression-evm/test-storagevar03.sh
+8,338 −6,722		test/regression-evm/test-sum-to-n-definition.kore
+12 −10		test/regression-evm/test-sum-to-n-spec.kore
+5 −2		test/regression-evm/test-sum-to-n.sh
+23,390 −11,850		test/regression-evm/test-totalSupply-definition.kore
+6 −6		test/regression-evm/test-totalSupply-spec.kore
+5 −2		test/regression-evm/test-totalSupply.sh
+2 −1		.gitignore
+1 −1		cabal.project
+1 −1		deps/haskell-backend_release
+1 −1		deps/k_release
+4 −4		flake.lock
+15 −2		flake.nix
+1 −13		library/Booster/Definition/Base.hs
+0 −8		library/Booster/Definition/Util.hs
+51 −33		library/Booster/JsonRpc.hs
+18 −18		library/Booster/JsonRpc/Utils.hs
+82 −44		library/Booster/Pattern/ApplyEquations.hs
+58 −80		library/Booster/Pattern/Base.hs
+20 −46		library/Booster/Pattern/Binary.hs
+133 −0		library/Booster/Pattern/Bool.hs
+1 −14		library/Booster/Pattern/Index.hs
+7 −86		library/Booster/Pattern/Match.hs
+9 −7		library/Booster/Pattern/Rewrite.hs
+0 −21		library/Booster/Pattern/Simplify.hs
+21 −29		library/Booster/Pattern/Util.hs
+39 −70		library/Booster/Syntax/Json/Externalise.hs
+60 −56		library/Booster/Syntax/Json/Internalise.hs
+119 −131		library/Booster/Syntax/ParsedKore/Internalise.hs
+3 −0		package.yaml
+21 −8		scripts/compare.py
+13 −7		scripts/performance-tests-kevm.sh
+18 −10		scripts/performance-tests-kontrol.sh
+1 −1		stack.yaml
+5 −5		stack.yaml.lock
+12 −0		stacklock2nix.patch
+0 −10		test/internalisation/bool.kore.report
+0 −2		test/internalisation/does-not-preserve-definedness.kore.report
+0 −2		test/internalisation/existentials.kore.report
+0 −33		test/internalisation/imp.kore.report
+0 −2		test/internalisation/preserves-definedness-total-function.kore.report
+0 −2		test/internalisation/preserves-definedness.kore.report
+0 −11		test/internalisation/subsorts.kore.report
+0 −44		test/internalisation/test-totalSupply-definition.kore.report
+57 −3		test/llvm-integration/LLVM.hs
+43 −0		test/llvm-integration/definition/llvm.k
+2 −2		tools/booster/Proxy.hs
+12 −5		unit-tests/Test/Booster/Fixture.hs
+44 −14		unit-tests/Test/Booster/Pattern/ApplyEquations.hs
+4 −16		unit-tests/Test/Booster/Pattern/Binary.hs
+19 −22		unit-tests/Test/Booster/Pattern/Rewrite.hs