Merge branch 'master' into bump-crucible

GaloisInc · Oct 21, 2024 · 370a731 · 370a731
2 parents 8c9f47c + d2fb176
commit 370a731
Show file tree

Hide file tree

Showing 28 changed files with 231 additions and 2,365 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -361,7 +361,7 @@ jobs:
 
         # If you change the entree-specs commit below, make sure you update the
         # documentation in saw-core-coq/README.md accordingly.
-      - run: opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#2ec3cab68797922dc2825bb6295dbdf6cfab9fbf
+      - run: opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#d871d0af37ffee757e3be1f8d776bd7e84399712
 
       # FIXME: the following steps generate Coq libraries for the SAW core to
       # Coq translator and builds them; if we do other Coq tests, these steps

diff --git a/CHANGES.md b/CHANGES.md
@@ -5,6 +5,8 @@
 * Counterexamples including SMT arrays are now printed with the array
   contents instead of placeholder text.
 
+* Due to the regressions seen in issues #1946 and #1944, the experimental compositional hardware verification work has been reverted.
+
 # Version 1.2 -- 2024-08-30
 
 ## New Features

diff --git a/intTests/test_comp_bisim/build.sh b/intTests/test_comp_bisim/build.sh
diff --git a/intTests/test_comp_bisim/clean.sh b/intTests/test_comp_bisim/clean.sh