diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index da9fc261086..14ce0266563 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -220,7 +220,7 @@ jobs:
 
   macos-build:
     name: 'Build MacOS Package'
-    runs-on: macos-11
+    runs-on: macos-13
     timeout-minutes: 120
     environment: production
     needs: [set-release-id, source-tarball]
@@ -273,7 +273,7 @@ jobs:
           git commit Formula/$PACKAGE.rb -m "Update ${PACKAGE} to ${VERSION}: part 1"
           ../kframework/package/macos/brew-build-and-update-to-local-bottle ${PACKAGE} ${VERSION} ${ROOT_URL}
           git reset HEAD^
-          LOCAL_BOTTLE_NAME=$(basename $(find . -name "kframework--${VERSION}.big_sur.bottle*.tar.gz"))
+          LOCAL_BOTTLE_NAME=$(basename $(find . -name "kframework--${VERSION}.ventura.bottle*.tar.gz"))
           BOTTLE_NAME=$(echo ${LOCAL_BOTTLE_NAME#./} | sed 's!kframework--!kframework-!')
           ../kframework/package/macos/brew-update-to-final ${PACKAGE} ${VERSION} ${ROOT_URL}
           echo "path=${LOCAL_BOTTLE_NAME}" >> ${GITHUB_OUTPUT}
diff --git a/flake.lock b/flake.lock
index 70d5de8654c..eb116e388aa 100644
--- a/flake.lock
+++ b/flake.lock
@@ -247,11 +247,11 @@
     "flake-compat_4": {
       "flake": false,
       "locked": {
-        "lastModified": 1673956053,
-        "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=",
+        "lastModified": 1696267196,
+        "narHash": "sha256-AAQ/2sD+0D18bb8hKuEEVpHUYD1GmO2Uh/taFamn6XQ=",
         "owner": "edolstra",
         "repo": "flake-compat",
-        "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9",
+        "rev": "4f910c9827911b1ec2bf26b5a062cd09f8d89f85",
         "type": "github"
       },
       "original": {
@@ -784,11 +784,11 @@
         "utils": "utils_2"
       },
       "locked": {
-        "lastModified": 1696083513,
-        "narHash": "sha256-zUlM3A0Q7IPE17QlDXRYV2iEmsitEwD0POwUYZPgIlo=",
+        "lastModified": 1696257790,
+        "narHash": "sha256-2iNcK72D4V9l+sjHBvv0ZAXXdSYf0YVX4MuaMvSxgb8=",
         "owner": "runtimeverification",
         "repo": "llvm-backend",
-        "rev": "a2577f4d26aaf04b654a2daa14b1586ccef959ea",
+        "rev": "0952940a242d8909da60d3ebde6059b47579f530",
         "type": "github"
       },
       "original": {
@@ -1227,11 +1227,11 @@
     },
     "nixpkgs_5": {
       "locked": {
-        "lastModified": 1695825837,
-        "narHash": "sha256-4Ne11kNRnQsmSJCRSSNkFRSnHC4Y5gPDBIQGjjPfJiU=",
+        "lastModified": 1696039360,
+        "narHash": "sha256-g7nIUV4uq1TOVeVIDEZLb005suTWCUjSY0zYOlSBsyE=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "5cfafa12d57374f48bcc36fda3274ada276cf69e",
+        "rev": "32dcb45f66c0487e92db8303a798ebc548cadedc",
         "type": "github"
       },
       "original": {
diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java
index b2fd5daa67a..d86230dbafa 100644
--- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java
+++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java
@@ -26,6 +26,7 @@ public List<Module> getKompileModules() {
         mods.add(new AbstractModule() {
             @Override
             protected void configure() {
+                binder().requireAtInjectOnConstructors();
                 bindOptions(HaskellBackendKModule.this::kompileOptions, binder());
                 installHaskellBackend(binder());
             }
@@ -54,6 +55,7 @@ public List<Module> getKRunModules() {
         return Collections.singletonList(new AbstractModule() {
             @Override
             protected void configure() {
+                binder().requireAtInjectOnConstructors();
                 installHaskellRewriter(binder());
             }
         });
@@ -74,6 +76,7 @@ public List<Module> getKProveModules() {
         return Collections.singletonList(new AbstractModule() {
             @Override
             protected void configure() {
+                binder().requireAtInjectOnConstructors();
                 installHaskellBackend(binder());
                 installHaskellRewriter(binder());
             }
diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java
index 5c20d442625..3a6649ef34c 100644
--- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java
+++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java
@@ -2,12 +2,15 @@
 package org.kframework.backend.haskell;
 
 import com.beust.jcommander.Parameter;
+import com.google.inject.Inject;
 import org.kframework.backend.kore.ModuleToKORE;
 import org.kframework.utils.inject.RequestScoped;
 import org.kframework.utils.options.BaseEnumConverter;
 
 @RequestScoped
 public class HaskellKRunOptions {
+    @Inject
+    public HaskellKRunOptions() {}
 
     @Parameter(names="--haskell-backend-command", descriptionKey = "command",
             description="Command to run the Haskell backend execution engine.", hidden = true)
diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java
index 69a9c8b4b2c..081be372136 100644
--- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java
+++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java
@@ -2,11 +2,14 @@
 package org.kframework.backend.haskell;
 
 import com.beust.jcommander.Parameter;
+import com.google.inject.Inject;
 import org.kframework.utils.inject.RequestScoped;
 
 @RequestScoped
 public class HaskellKompileOptions {
 
+    @Inject
+    public HaskellKompileOptions() {}
     @Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.", descriptionKey = "command", hidden = true)
     public String haskellBackendCommand = "kore-exec";
 
diff --git a/k-distribution/src/main/assembly/bin.xml b/k-distribution/src/main/assembly/bin.xml
index 3ea8529e2bd..d322cd42ab8 100644
--- a/k-distribution/src/main/assembly/bin.xml
+++ b/k-distribution/src/main/assembly/bin.xml
@@ -69,7 +69,7 @@
     </fileSet>
     <fileSet>
       <directory>${project.parent.basedir}/package</directory>
-      <outputDirectory>/lib</outputDirectory>
+      <outputDirectory>/lib/kframework</outputDirectory>
       <includes>
         <include>version</include>
       </includes>
diff --git a/k-distribution/src/main/scripts/bin/krun b/k-distribution/src/main/scripts/bin/krun
index 7f684964a01..e5e88599fe4 100755
--- a/k-distribution/src/main/scripts/bin/krun
+++ b/k-distribution/src/main/scripts/bin/krun
@@ -37,12 +37,16 @@ filterSubst=
 if [[ "$OSTYPE" == "darwin"* ]]; then
   LLDB_FILE="$(dirname "$0")/../lib/kllvm/lldb/k_lldb_path"
   if [ -f "$LLDB_FILE" ]; then
-    DBG_CMD="$(cat "$LLDB_FILE") -- "
+    DBG_EXE="$(cat "$LLDB_FILE")"
   else
-    DBG_CMD="lldb --"
+    DBG_EXE="lldb"
   fi
+  DBG_CMD=" --"
+  DBG_FLAG=" -s "
 else
-  DBG_CMD="gdb --args "
+  DBG_EXE="gdb"
+  DBG_FLAG=" -x "
+  DBG_CMD=" --args "
 fi
 
 
@@ -112,6 +116,10 @@ $KRUN options:
                            parser. This can be overridden with -p.
       --debugger           Launch the backend in a debugging console.
                            Currently only supported on LLVM backend.
+      --debugger-batch     Launch the backend in a debugging console in batch
+                           mode. Currently only supported on LLVM backend.
+      --debugger-command FILE  Execute GDB commands from FILE to debug program.
+                               Currently only supported on LLVM backend.
   -d, --directory DIR      [DEPRECATED] Look for a kompiled directory ending in "-kompiled"
                            under the directory DIR.
       --dry-run            Do not execute backend, but instead print the
@@ -392,9 +400,24 @@ do
       ;;
 
       --debugger)
-      cmdprefix="$DBG_CMD"
+      cmdprefix="$DBG_EXE $DBG_CMD"
       ;;
 
+      --debugger-command)
+        debugCommandFile="$2"
+        cmdprefix="$DBG_EXE $DBG_FLAG $debugCommandFile $DBG_CMD"
+      shift
+      ;;
+
+      --debugger-batch)
+      if [[ $cmdprefix == *gdb* || $cmdprefix == *lldb* ]]; then
+        cmdprefix="$DBG_EXE --batch $DBG_FLAG $debugCommandFile $DBG_CMD"
+      else
+        DBG_CMD=" --batch $DBG_CMD"
+      fi
+      ;;
+
+
       --statistics)
       statistics=true
       ;;
diff --git a/k-distribution/src/test/scala/org/kframework/backend/kore/KoreTest.scala b/k-distribution/src/test/scala/org/kframework/backend/kore/KoreTest.scala
index d35afda1970..d6804496815 100644
--- a/k-distribution/src/test/scala/org/kframework/backend/kore/KoreTest.scala
+++ b/k-distribution/src/test/scala/org/kframework/backend/kore/KoreTest.scala
@@ -65,18 +65,28 @@ class KoreTest {
     attributes.patterns.exists { case p: Application => p.head.ctr == name }
   }
 
+  // get the rewrite associated with a rule or equational axiom
+  //
+  // \and(\equals(requires, \dv("true")), \and(_, \rewrites(lhs, rhs)))
+  // \and(\top(), \and(_, \rewrites(lhs, rhs)))
+  // \rewrites(\and(\equals(requires, \dv("true")), lhs), \and(_, rhs))
+  // \rewrites(\and(\top(), lhs), \and(_, rhs))
+  // \implies(\equals(requires, \dv("true")), \and(\equals(lhs, rhs), _))
+  // \implies(\top, \and(\equals(lhs, rhs), _))
+  // \implies(\and(_, \equals(requires, \dv("true"))), \and(\equals(lhs, rhs), _))
+  // \implies(\and(_, \top), \and(\equals(lhs, rhs), _))
+  // \equals(lhs, rhs)
   def getRewrite(axiom: AxiomDeclaration): Option[GeneralizedRewrite] = {
     def go(pattern: Pattern): Option[GeneralizedRewrite] = {
       pattern match {
-        case And(_, Equals(_, _, _, _), And(_, _, rw @ Rewrites(_, _, _))) => Some(rw)
-        case And(_, Top(_), And(_, _, rw @ Rewrites(_, _, _))) => Some(rw)
-        case Rewrites(s, And(_, Equals(_, _, _, _), l), And(_, _, r)) => Some(B.Rewrites(s, l, r))
-        case Rewrites(s, And(_, Top(_), l), And(_, _, r)) => Some(B.Rewrites(s, l, r))
-        case Implies(_, Bottom(_), p) => go(p)
-        case Implies(_, Equals(_, _, _, _), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq)
-        case Implies(_, Top(_), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq)
-        case Implies(_, And(_, _, Equals(_, _, _, _)), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq)
-        case Implies(_, And(_, _, Top(_)), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq)
+        case And(_, Equals(_, _, _, _) +: And(_, _ +: (rw @ Rewrites(_, _, _)) +: Seq()) +: Seq()) => Some(rw)
+        case And(_, Top(_) +: And(_, _ +: (rw @ Rewrites(_, _, _)) +: Seq()) +: Seq()) => Some(rw)
+        case Rewrites(s, And(_, Equals(_, _, _, _) +: l +: Seq()), And(_, _ +: r +: Seq())) => Some(B.Rewrites(s, l, r))
+        case Rewrites(s, And(_, Top(_) +: l +: Seq()), And(_, _ +: r +: Seq())) => Some(B.Rewrites(s, l, r))
+        case Implies(_, Equals(_, _, _, _), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
+        case Implies(_, Top(_), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
+        case Implies(_, And(_, _ +: Equals(_, _, _, _) +: Seq()), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
+        case Implies(_, And(_, _ +: Top(_) +: Seq()), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
         case eq @ Equals(_, _, Application(_, _), _) => Some(eq)
         case _ => None
 
@@ -91,7 +101,7 @@ class KoreTest {
 
   def symbols(pat: Pattern): Seq[SymbolOrAlias] = {
     pat match {
-      case And(_, p1, p2) => symbols(p1) ++ symbols(p2)
+      case And(_, ps) => ps.flatMap(symbols)
       case Application(s, ps) => Seq(s).filter(isConcrete) ++ ps.flatMap(symbols)
       case Ceil(_, _, p) => symbols(p)
       case Equals(_, _, p1, p2) => symbols(p1) ++ symbols(p2)
@@ -103,7 +113,7 @@ class KoreTest {
       case Mem(_, _, p1, p2) => symbols(p1) ++ symbols(p2)
 //      case Next(_, p) => symbols(p)
       case Not(_, p) => symbols(p)
-      case Or(_, p1, p2) => symbols(p1) ++ symbols(p2)
+      case Or(_, ps) => ps.flatMap(symbols)
       case Rewrites(_, p1, p2) => symbols(p1) ++ symbols(p2)
       case _ => Seq()
     }
diff --git a/kernel/pom.xml b/kernel/pom.xml
index c932c02dcc6..aa1541af51d 100644
--- a/kernel/pom.xml
+++ b/kernel/pom.xml
@@ -32,13 +32,13 @@
     <dependency>
       <groupId>com.google.inject</groupId>
       <artifactId>guice</artifactId>
-      <version>4.0-beta5</version>
+      <version>4.0</version>
       <classifier>no_aop</classifier>
     </dependency>
     <dependency>
       <groupId>com.google.inject.extensions</groupId>
       <artifactId>guice-multibindings</artifactId>
-      <version>4.0-beta5</version>
+      <version>4.0</version>
       <exclusions>
         <exclusion>
           <groupId>com.google.inject</groupId>
@@ -49,7 +49,7 @@
     <dependency>
       <groupId>com.google.inject.extensions</groupId>
       <artifactId>guice-grapher</artifactId>
-      <version>4.0-beta5</version>
+      <version>4.0</version>
       <exclusions>
         <exclusion>
           <groupId>com.google.inject</groupId>
@@ -60,7 +60,7 @@
     <dependency>
       <groupId>com.google.inject.extensions</groupId>
       <artifactId>guice-throwingproviders</artifactId>
-      <version>4.0-beta5</version>
+      <version>4.0</version>
       <exclusions>
         <exclusion>
           <groupId>com.google.inject</groupId>
diff --git a/kernel/src/main/java/org/kframework/kast/KastModule.java b/kernel/src/main/java/org/kframework/kast/KastModule.java
index aeb3976a48d..a28605ce26d 100644
--- a/kernel/src/main/java/org/kframework/kast/KastModule.java
+++ b/kernel/src/main/java/org/kframework/kast/KastModule.java
@@ -21,6 +21,7 @@ public class KastModule extends AbstractModule {
 
     @Override
     public void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(FrontEnd.class).to(KastFrontEnd.class);
         bind(Tool.class).toInstance(Tool.KAST);
 
diff --git a/kernel/src/main/java/org/kframework/kast/KastOptions.java b/kernel/src/main/java/org/kframework/kast/KastOptions.java
index add6323ceb2..7ef74e430c6 100644
--- a/kernel/src/main/java/org/kframework/kast/KastOptions.java
+++ b/kernel/src/main/java/org/kframework/kast/KastOptions.java
@@ -31,6 +31,9 @@
 @RequestScoped
 public final class KastOptions {
 
+    @Inject
+    public KastOptions() {}
+
     @Parameter(description="<file>")
     private List<String> parameters;
 
diff --git a/kernel/src/main/java/org/kframework/kdep/KDepModule.java b/kernel/src/main/java/org/kframework/kdep/KDepModule.java
index c068f105368..ed6af4762b9 100644
--- a/kernel/src/main/java/org/kframework/kdep/KDepModule.java
+++ b/kernel/src/main/java/org/kframework/kdep/KDepModule.java
@@ -22,7 +22,7 @@
 public class KDepModule extends AbstractModule {
     @Override
     protected void configure() {
-
+        binder().requireAtInjectOnConstructors();
         bind(FrontEnd.class).to(KDepFrontEnd.class);
         bind(Tool.class).toInstance(Tool.KDEP);
 
diff --git a/kernel/src/main/java/org/kframework/kdep/KDepOptions.java b/kernel/src/main/java/org/kframework/kdep/KDepOptions.java
index d830c3b8bf3..c65cc98273e 100644
--- a/kernel/src/main/java/org/kframework/kdep/KDepOptions.java
+++ b/kernel/src/main/java/org/kframework/kdep/KDepOptions.java
@@ -3,6 +3,7 @@
 
 import com.beust.jcommander.Parameter;
 import com.beust.jcommander.ParametersDelegate;
+import com.google.inject.Inject;
 import org.kframework.main.GlobalOptions;
 import org.kframework.utils.inject.RequestScoped;
 import org.kframework.utils.options.OuterParsingOptions;
@@ -16,6 +17,9 @@
 @RequestScoped
 public class KDepOptions {
 
+    @Inject
+    public KDepOptions() {}
+
     @ParametersDelegate
     public transient GlobalOptions global = new GlobalOptions();
 
diff --git a/kernel/src/main/java/org/kframework/kil/loader/Context.java b/kernel/src/main/java/org/kframework/kil/loader/Context.java
index 2bc8a8252db..a136a3922e6 100644
--- a/kernel/src/main/java/org/kframework/kil/loader/Context.java
+++ b/kernel/src/main/java/org/kframework/kil/loader/Context.java
@@ -19,6 +19,9 @@
 @RequestScoped
 public class Context implements Serializable {
 
+    @Inject
+    public Context() {}
+
     /**
      * Represents a map from all Klabels or attributes in string representation
      * to sets of corresponding productions.
diff --git a/kernel/src/main/java/org/kframework/kompile/BackendModule.java b/kernel/src/main/java/org/kframework/kompile/BackendModule.java
index 35b91d2654f..5425cabee5c 100644
--- a/kernel/src/main/java/org/kframework/kompile/BackendModule.java
+++ b/kernel/src/main/java/org/kframework/kompile/BackendModule.java
@@ -14,6 +14,7 @@
 public class BackendModule extends AbstractModule {
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         MapBinder<String, Backend> backendBinder = MapBinder.newMapBinder(
                 binder(), String.class, org.kframework.compile.Backend.class);
         backendBinder.addBinding("kore").to(KoreBackend.class);
diff --git a/kernel/src/main/java/org/kframework/kompile/KompileModule.java b/kernel/src/main/java/org/kframework/kompile/KompileModule.java
index 10ed758e44e..3757d7c6432 100644
--- a/kernel/src/main/java/org/kframework/kompile/KompileModule.java
+++ b/kernel/src/main/java/org/kframework/kompile/KompileModule.java
@@ -25,6 +25,7 @@ public KompileModule() {
 
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(FrontEnd.class).to(KompileFrontEnd.class);
         bind(Tool.class).toInstance(Tool.KOMPILE);
 
diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java
index 8d494435b6d..ba96c409fdd 100644
--- a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java
+++ b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java
@@ -3,6 +3,7 @@
 
 import com.beust.jcommander.Parameter;
 import com.beust.jcommander.ParametersDelegate;
+import com.google.inject.Inject;
 import org.apache.commons.io.FilenameUtils;
 import org.kframework.backend.Backends;
 import org.kframework.main.GlobalOptions;
@@ -23,7 +24,8 @@
 
 @RequestScoped
 public class KompileOptions implements Serializable {
-
+    @Inject
+    public KompileOptions() {}
 
     /**
      * WARNING: this field will be non-null in kompile tool, but null when KompileOption is deserialized,
diff --git a/kernel/src/main/java/org/kframework/kprove/KProveModule.java b/kernel/src/main/java/org/kframework/kprove/KProveModule.java
index 84b17c42eb3..ca375b76ad7 100644
--- a/kernel/src/main/java/org/kframework/kprove/KProveModule.java
+++ b/kernel/src/main/java/org/kframework/kprove/KProveModule.java
@@ -20,6 +20,7 @@
 public class KProveModule extends AbstractModule {
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(FrontEnd.class).to(KProveFrontEnd.class);
         bind(Tool.class).toInstance(Tool.KPROVE);
 
diff --git a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java
index b5b59d83917..d25a5b6b6c3 100644
--- a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java
+++ b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java
@@ -4,6 +4,7 @@
 
 import com.beust.jcommander.Parameter;
 import com.beust.jcommander.ParametersDelegate;
+import com.google.inject.Inject;
 import org.kframework.unparser.PrintOptions;
 import org.kframework.main.GlobalOptions;
 import org.kframework.utils.file.FileUtil;
@@ -20,6 +21,8 @@
 
 @RequestScoped
 public class KProveOptions {
+    @Inject
+    public KProveOptions() {}
 
     @ParametersDelegate
     private final transient GlobalOptions global = new GlobalOptions();
diff --git a/kernel/src/main/java/org/kframework/kprove/RewriterModule.java b/kernel/src/main/java/org/kframework/kprove/RewriterModule.java
index 5670711aa9b..90ea42f76b8 100644
--- a/kernel/src/main/java/org/kframework/kprove/RewriterModule.java
+++ b/kernel/src/main/java/org/kframework/kprove/RewriterModule.java
@@ -17,6 +17,7 @@
 public class RewriterModule extends AbstractModule {
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(FileUtil.class);
     }
 
diff --git a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java
index 2ae3035c72b..93328edf004 100644
--- a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java
+++ b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java
@@ -22,6 +22,7 @@
 public class KSearchPatternModule extends AbstractModule {
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(FrontEnd.class).to(KSearchPatternFrontEnd.class);
         bind(Tool.class).toInstance(Tool.KSEARCHPATTERN);
 
diff --git a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java
index 1c2d9a32a08..9fcc1baec84 100644
--- a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java
+++ b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java
@@ -3,6 +3,7 @@
 
 import com.beust.jcommander.Parameter;
 import com.beust.jcommander.ParametersDelegate;
+import com.google.inject.Inject;
 import org.kframework.main.GlobalOptions;
 import org.kframework.utils.inject.RequestScoped;
 import org.kframework.utils.options.DefinitionLoadingOptions;
@@ -16,6 +17,9 @@
 @RequestScoped
 public class KSearchPatternOptions {
 
+    @Inject
+    public KSearchPatternOptions() {}
+
     @ParametersDelegate
     public transient GlobalOptions global = new GlobalOptions();
 
diff --git a/kernel/src/main/java/org/kframework/kserver/KServerModule.java b/kernel/src/main/java/org/kframework/kserver/KServerModule.java
index f8e9f4d57bb..865cdfc76f4 100644
--- a/kernel/src/main/java/org/kframework/kserver/KServerModule.java
+++ b/kernel/src/main/java/org/kframework/kserver/KServerModule.java
@@ -20,6 +20,7 @@ public class KServerModule extends AbstractModule {
 
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(Tool.class).toInstance(Tool.KSERVER);
         bind(FrontEnd.class).to(KServerFrontEnd.class);
 
diff --git a/kernel/src/main/java/org/kframework/kserver/KServerOptions.java b/kernel/src/main/java/org/kframework/kserver/KServerOptions.java
index 322b689b874..b09695b0ac3 100644
--- a/kernel/src/main/java/org/kframework/kserver/KServerOptions.java
+++ b/kernel/src/main/java/org/kframework/kserver/KServerOptions.java
@@ -1,6 +1,7 @@
 // Copyright (c) K Team. All Rights Reserved.
 package org.kframework.kserver;
 
+import com.google.inject.Inject;
 import org.kframework.main.GlobalOptions;
 import org.kframework.utils.inject.RequestScoped;
 
@@ -10,6 +11,9 @@
 @RequestScoped
 public class KServerOptions {
 
+    @Inject
+    public KServerOptions() {}
+
     @ParametersDelegate
     public transient GlobalOptions global = new GlobalOptions();
 
diff --git a/kernel/src/main/java/org/kframework/main/AbstractKModule.java b/kernel/src/main/java/org/kframework/main/AbstractKModule.java
index 9fc12a9cb48..2a8dd35361b 100644
--- a/kernel/src/main/java/org/kframework/main/AbstractKModule.java
+++ b/kernel/src/main/java/org/kframework/main/AbstractKModule.java
@@ -37,6 +37,7 @@ public List<Pair<Class<?>, Boolean>> kproveOptions() {
     }
 
     protected void bindOptions(Supplier<List<Pair<Class<?>, Boolean>>> action, Binder binder) {
+        binder.requireAtInjectOnConstructors();
         Multibinder<Object> optionsBinder = Multibinder.newSetBinder(binder, Object.class, Options.class);
         for (Pair<Class<?>, Boolean> option : action.get()) {
             optionsBinder.addBinding().to(option.getKey());
@@ -81,6 +82,7 @@ public List<Module> getDefinitionSpecificKEqModules() {
 
             @Override
             protected void configure() {
+                binder().requireAtInjectOnConstructors();
                 //bind backend implementations of tools to their interfaces
             }
         });
diff --git a/kernel/src/main/java/org/kframework/main/FrontEnd.java b/kernel/src/main/java/org/kframework/main/FrontEnd.java
index 7417d75ee92..08e015488e0 100644
--- a/kernel/src/main/java/org/kframework/main/FrontEnd.java
+++ b/kernel/src/main/java/org/kframework/main/FrontEnd.java
@@ -2,6 +2,7 @@
 package org.kframework.main;
 
 import com.beust.jcommander.ParameterException;
+import com.google.inject.Inject;
 import com.google.inject.Provider;
 import org.kframework.utils.ExitOnTimeoutThread;
 import org.kframework.utils.InterrupterRunnable;
@@ -22,6 +23,7 @@ public abstract class FrontEnd {
     private final JarInfo jarInfo;
     private final Provider<FileUtil> files;
 
+    @Inject
     public FrontEnd(
             KExceptionManager kem,
             GlobalOptions globalOptions,
diff --git a/kernel/src/main/java/org/kframework/main/GlobalOptions.java b/kernel/src/main/java/org/kframework/main/GlobalOptions.java
index f0ae7d82c66..d78fad84535 100644
--- a/kernel/src/main/java/org/kframework/main/GlobalOptions.java
+++ b/kernel/src/main/java/org/kframework/main/GlobalOptions.java
@@ -19,13 +19,6 @@ public final class GlobalOptions {
 
     public GlobalOptions() {}
 
-    //TODO(dwightguth): remove in Guice 4.0
-    /**
-     * Prevents instantiation by Guice when not explicitly configured in a Module.
-     */
-    @Inject
-    public GlobalOptions(Void v) {}
-
     public GlobalOptions(boolean debug, Warnings warnings, boolean verbose) {
         this.debug = debug;
         this.warnings = warnings;
diff --git a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java b/kernel/src/main/java/org/kframework/unparser/PrintOptions.java
index c74146e45ea..74c860c80da 100644
--- a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java
+++ b/kernel/src/main/java/org/kframework/unparser/PrintOptions.java
@@ -23,14 +23,6 @@ public PrintOptions(OutputModes output) {
         this.output = output;
     }
 
-    //TODO(dwightguth): remove in Guice 4.0
-    /**
-     * Prevents instantiation by Guice when not explicitly configured in a Module.
-     */
-    @Inject
-    public PrintOptions(Void v) {
-    }
-
     @Parameter(names = "--color", description = "Use colors in output. Default is on.", descriptionKey = "mode",
             converter=ColorModeConverter.class)
     private ColorSetting color;
diff --git a/kernel/src/main/java/org/kframework/utils/file/JarInfo.java b/kernel/src/main/java/org/kframework/utils/file/JarInfo.java
index 5661f04c76e..adc55aebe1c 100644
--- a/kernel/src/main/java/org/kframework/utils/file/JarInfo.java
+++ b/kernel/src/main/java/org/kframework/utils/file/JarInfo.java
@@ -85,7 +85,7 @@ public void printVersionMessage() {
             // the release version if we're not (e.g. from a release tarball).
             String version = mf.getMainAttributes().getValue("Implementation-Git-Describe");
             if (version.isEmpty()) {
-                version = "v" + FileUtils.readFileToString(new File(kBase + "/lib/version")).trim();
+                version = "v" + FileUtils.readFileToString(new File(kBase + "/lib/kframework/version")).trim();
             }
 
             System.out.println("K version:    " + version);
diff --git a/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java b/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java
index 1eedd8619c1..bb1a47f6d2c 100644
--- a/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java
+++ b/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java
@@ -22,6 +22,7 @@ public class CommonModule extends AbstractModule {
 
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         SimpleScope requestScope = new SimpleScope();
         bindScope(RequestScoped.class, requestScope);
         DefinitionScope definitionScope = new DefinitionScope();
diff --git a/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java b/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java
index d093fdf0228..9f3f60084de 100644
--- a/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java
+++ b/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java
@@ -27,6 +27,7 @@ public class DefinitionLoadingModule extends AbstractModule {
 
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
     }
 
     @Provides @DefinitionScoped
diff --git a/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java b/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java
index 5c5f2c87414..495db016164 100644
--- a/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java
+++ b/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java
@@ -31,6 +31,7 @@ public class JCommanderModule extends AbstractModule  {
 
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(String[].class).annotatedWith(Options.class)
             .toProvider(SimpleScope.seededKeyProvider()).in(RequestScoped.class);;
     }
diff --git a/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java b/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java
index f6f0a7eec3c..cdb86466444 100644
--- a/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java
+++ b/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java
@@ -27,7 +27,7 @@ public class OuterParsingModule extends AbstractModule {
 
     @Override
     protected void configure() {
-
+        binder().requireAtInjectOnConstructors();
     }
 
     @Provides
diff --git a/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java b/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java
index 2046937054e..14c57e748d1 100644
--- a/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java
+++ b/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java
@@ -10,10 +10,6 @@ public class BackendOptions implements Serializable {
 
     public BackendOptions() {}
 
-    //TODO(dwightguth): remove in Guice 4.0
-    @Inject
-    public BackendOptions(Void v) {}
-
     @Parameter(names="--dry-run", description="Compile program into KORE format but do not run. Only used in Haskell and LLVM backend.")
     public boolean dryRun = false;
 }
diff --git a/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java b/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java
index 8f9ed1b7b41..a4d1c9c4f8b 100644
--- a/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java
+++ b/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java
@@ -8,10 +8,6 @@ public class DefinitionLoadingOptions {
 
     public DefinitionLoadingOptions() {}
 
-    //TODO(dwightguth): remove in Guice 4.0
-    @Inject
-    public DefinitionLoadingOptions(Void v) {}
-
     @Parameter(names={"--directory", "-d"}, description="[DEPRECATED] Path to the directory in which the kompiled " +
             "K definition resides. The default is the unique, only directory with the suffix '-kompiled' " +
             "in the current directory.", descriptionKey = "path", hidden = true)
diff --git a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
index b1acb132943..9fd7cc13a32 100644
--- a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
+++ b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
@@ -10,12 +10,7 @@ public class SMTOptions implements Serializable {
 
     public SMTOptions() {}
 
-    //TODO(dwightguth): remove in Guice 4.0
-    @Inject
-    public SMTOptions(Void v) {}
-
-    @Parameter(names="--smt", descriptionKey = "executable", converter=SMTSolverConverter.class,
-            description="SMT solver to use for checking constraints. <executable> is one of [z3|none].", hidden = true)
+    @Parameter(names="--smt", converter=SMTSolverConverter.class, description="SMT solver to use for checking constraints. <executable> is one of [z3|none].", descriptionKey = "executable", hidden = true)
     public SMTSolver smt = SMTSolver.Z3;
 
     public static class SMTSolverConverter extends BaseEnumConverter<SMTSolver> {
diff --git a/kernel/src/test/java/org/kframework/utils/BaseTestCase.java b/kernel/src/test/java/org/kframework/utils/BaseTestCase.java
index 17212387f6a..4ccafc4829a 100644
--- a/kernel/src/test/java/org/kframework/utils/BaseTestCase.java
+++ b/kernel/src/test/java/org/kframework/utils/BaseTestCase.java
@@ -71,6 +71,7 @@ public class DefinitionSpecificTestModule extends AbstractModule {
 
         @Override
         protected void configure() {
+            binder().requireAtInjectOnConstructors();
             bind(KompileOptions.class).toInstance(context.kompileOptions);
             bind(Definition.class).toInstance(definition);
             bind(File.class).annotatedWith(KompiledDir.class).toInstance(kompiledDir);
@@ -88,6 +89,7 @@ public class TestModule extends AbstractModule {
 
         @Override
         protected void configure() {
+            binder().requireAtInjectOnConstructors();
             bind(RunProcess.class).toInstance(rp);
             bind(KastOptions.class).toInstance(new KastOptions());
         }
diff --git a/kore/src/main/scala/org/kframework/parser/kore/Default.scala b/kore/src/main/scala/org/kframework/parser/kore/Default.scala
index 2f80fc53674..01df2ccf620 100644
--- a/kore/src/main/scala/org/kframework/parser/kore/Default.scala
+++ b/kore/src/main/scala/org/kframework/parser/kore/Default.scala
@@ -40,17 +40,9 @@ object implementation {
 
     case class Bottom(s: i.Sort) extends i.Bottom
 
-    case class And(s: i.Sort, args: Seq[i.Pattern]) extends i.And {
-      val _1 = args(0)
+    case class And(s: i.Sort, args: Seq[i.Pattern]) extends i.And
 
-      val _2 = args(1)
-    }
-
-    case class Or(s: i.Sort, args: Seq[i.Pattern]) extends i.Or {
-      val _1 = args(0)
-
-      val _2 = args(1)
-    }
+    case class Or(s: i.Sort, args: Seq[i.Pattern]) extends i.Or
 
     case class Not(s: i.Sort, _1: i.Pattern) extends i.Not
 
@@ -138,11 +130,23 @@ object implementation {
 
     def And(s: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Pattern = d.And(s, Seq(_1, _2))
 
-    def And(s: i.Sort, args: Seq[i.Pattern]): i.Pattern = d.And(s, args)
+    def And(s: i.Sort, args: Seq[i.Pattern]): i.Pattern = {
+      args.size match {
+        case 0 => Top(s)
+        case 1 => args(0)
+        case _ => d.And(s, args)
+      }
+    }
 
     def Or(s: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Pattern = d.Or(s, Seq(_1, _2))
 
-    def Or(s: i.Sort, args: Seq[i.Pattern]): i.Pattern = d.Or(s, args)
+    def Or(s: i.Sort, args: Seq[i.Pattern]): i.Pattern = {
+      args.size match {
+        case 0 => Bottom(s)
+        case 1 => args(0)
+        case _ => d.Or(s, args)
+      }
+    }
 
     def Not(s: i.Sort, _1: i.Pattern): i.Pattern = d.Not(s, _1)
 
diff --git a/kore/src/main/scala/org/kframework/parser/kore/Interface.scala b/kore/src/main/scala/org/kframework/parser/kore/Interface.scala
index 6723c1342c7..ba7f6d0221c 100644
--- a/kore/src/main/scala/org/kframework/parser/kore/Interface.scala
+++ b/kore/src/main/scala/org/kframework/parser/kore/Interface.scala
@@ -164,29 +164,21 @@ object Bottom {
 trait And extends Pattern {
   def s: Sort
 
-  def _1: Pattern
-
-  def _2: Pattern
-
   def args: Seq[Pattern]
 }
 
 object And {
-  def unapply(arg: And): Option[(Sort, Pattern, Pattern)] = Some(arg.s, arg._1, arg._2)
+  def unapply(arg: And): Option[(Sort, Seq[Pattern])] = Some(arg.s, arg.args)
 }
 
 trait Or extends Pattern {
   def s: Sort
 
-  def _1: Pattern
-
-  def _2: Pattern
-
   def args: Seq[Pattern]
 }
 
 object Or {
-  def unapply(arg: Or): Option[(Sort, Pattern, Pattern)] = Some(arg.s, arg._1, arg._2)
+  def unapply(arg: Or): Option[(Sort, Seq[Pattern])] = Some(arg.s, arg.args)
 }
 
 trait Not extends Pattern {
diff --git a/kore/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala b/kore/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala
index ec1f8b0c51d..539cf201420 100644
--- a/kore/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala
+++ b/kore/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala
@@ -2,6 +2,7 @@
 package org.kframework.parser.kore.parser
 
 import org.kframework.builtin.{KLabels, Sorts}
+import org.kframework.kore.Assoc
 import org.kframework.kore.KVariable
 import org.kframework.kore.KORE
 import org.kframework.attributes.Att
@@ -133,10 +134,12 @@ class KoreToK (sortAtt : Map[String, String]) {
       KORE.KApply(KORE.KLabel(KLabels.ML_TRUE.name, apply(s)))
     case kore.Bottom(s) =>
       KORE.KApply(KORE.KLabel(KLabels.ML_FALSE.name, apply(s)))
-    case kore.And(s, p, q) =>
-      KORE.KApply(KORE.KLabel(KLabels.ML_AND.name, apply(s)), apply(p), apply(q))
-    case kore.Or(s, p, q) =>
-      KORE.KApply(KORE.KLabel(KLabels.ML_OR.name, apply(s)), apply(p), apply(q))
+    case kore.And(s, items) =>
+      val and = KORE.KLabel(KLabels.ML_AND.name, apply(s))
+      KORE.KApply(and,  Assoc.flatten(and, items.map(apply), KORE.KLabel(KLabels.ML_TRUE.name, apply(s))))
+    case kore.Or(s, items) =>
+      val or = KORE.KLabel(KLabels.ML_OR.name, apply(s))
+      KORE.KApply(or,  Assoc.flatten(or, items.map(apply), KORE.KLabel(KLabels.ML_FALSE.name, apply(s))))
     case kore.Not(s, p) =>
       KORE.KApply(KORE.KLabel(KLabels.ML_NOT.name, apply(s)), apply(p))
     case kore.Implies(s, p, q) =>
diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java
index e81ce93f110..bb757de59a8 100644
--- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java
+++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java
@@ -3,6 +3,7 @@
 
 import com.beust.jcommander.Parameter;
 import com.beust.jcommander.IStringConverter;
+import com.google.inject.Inject;
 import org.kframework.utils.inject.RequestScoped;
 
 import java.util.Arrays;
@@ -12,6 +13,9 @@
 @RequestScoped
 public class LLVMKompileOptions {
 
+    @Inject
+    public LLVMKompileOptions() {}
+
     @Parameter(names="--enable-llvm-debug", description="Enable debugging support for the LLVM backend.")
     public boolean debug = false;
 
diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend
index a2577f4d26a..0952940a242 160000
--- a/llvm-backend/src/main/native/llvm-backend
+++ b/llvm-backend/src/main/native/llvm-backend
@@ -1 +1 @@
-Subproject commit a2577f4d26aaf04b654a2daa14b1586ccef959ea
+Subproject commit 0952940a242d8909da60d3ebde6059b47579f530
diff --git a/nix/mavenix.lock b/nix/mavenix.lock
index 7be2b7a378a..541407e5860 100644
--- a/nix/mavenix.lock
+++ b/nix/mavenix.lock
@@ -282,52 +282,52 @@
       "sha1": "1b77ba79f9b2b7dfd4e15ea7bb0d568d5eb9cb8d"
     },
     {
-      "path": "com/google/inject/extensions/extensions-parent/4.0-beta5/extensions-parent-4.0-beta5.pom",
-      "sha1": "516d8e5e771cd573364dc6ff53c2c6c13908a713"
+      "path": "com/google/inject/extensions/extensions-parent/4.0/extensions-parent-4.0.pom",
+      "sha1": "db8e45ab989a2347421ff0d32be5446528d6f63f"
     },
     {
-      "path": "com/google/inject/extensions/guice-assistedinject/4.0-beta5/guice-assistedinject-4.0-beta5.jar",
-      "sha1": "820f10e0650cd9ed2591f398937df50f330b147d"
+      "path": "com/google/inject/extensions/guice-assistedinject/4.0/guice-assistedinject-4.0.jar",
+      "sha1": "8fa6431da1a2187817e3e52e967535899e2e46ca"
     },
     {
-      "path": "com/google/inject/extensions/guice-assistedinject/4.0-beta5/guice-assistedinject-4.0-beta5.pom",
-      "sha1": "4b9b352e0537b0ca49cb97533387864b185df09b"
+      "path": "com/google/inject/extensions/guice-assistedinject/4.0/guice-assistedinject-4.0.pom",
+      "sha1": "00c7fc29684b20dd475f517d5dafc850c613efde"
     },
     {
-      "path": "com/google/inject/extensions/guice-grapher/4.0-beta5/guice-grapher-4.0-beta5.jar",
-      "sha1": "dd9a00d72fecfa05a77bf28c7922eacddda23b18"
+      "path": "com/google/inject/extensions/guice-grapher/4.0/guice-grapher-4.0.jar",
+      "sha1": "4e611ae9b12bfc4ddd430a58c65ba1c4328eeaf9"
     },
     {
-      "path": "com/google/inject/extensions/guice-grapher/4.0-beta5/guice-grapher-4.0-beta5.pom",
-      "sha1": "1cd692901e55d382cdb9e647d74617bb68d63126"
+      "path": "com/google/inject/extensions/guice-grapher/4.0/guice-grapher-4.0.pom",
+      "sha1": "86b9c4937ebba7d14054d0f025f0df51d071218d"
     },
     {
-      "path": "com/google/inject/extensions/guice-multibindings/4.0-beta5/guice-multibindings-4.0-beta5.jar",
-      "sha1": "f432356db0a167127ffe4a7921238d7205b12682"
+      "path": "com/google/inject/extensions/guice-multibindings/4.0/guice-multibindings-4.0.jar",
+      "sha1": "f4509545b4470bbcc865aa500ad6fef2e97d28bf"
     },
     {
-      "path": "com/google/inject/extensions/guice-multibindings/4.0-beta5/guice-multibindings-4.0-beta5.pom",
-      "sha1": "3cff7b7b5f418f5edca0fa1b0d4bcd3f3215d9c7"
+      "path": "com/google/inject/extensions/guice-multibindings/4.0/guice-multibindings-4.0.pom",
+      "sha1": "2387a1e5163308cd826b348db825973df0800ad3"
     },
     {
-      "path": "com/google/inject/extensions/guice-throwingproviders/4.0-beta5/guice-throwingproviders-4.0-beta5.jar",
-      "sha1": "8840bd8267a5b09ee84a314a54dbdc6c1b0a7efb"
+      "path": "com/google/inject/extensions/guice-throwingproviders/4.0/guice-throwingproviders-4.0.jar",
+      "sha1": "90876169e80b4db9b61d654367c4c55079ae4e91"
     },
     {
-      "path": "com/google/inject/extensions/guice-throwingproviders/4.0-beta5/guice-throwingproviders-4.0-beta5.pom",
-      "sha1": "cb52affb5a89e66a5f1d9ab3a7fde7dda1cc5baa"
+      "path": "com/google/inject/extensions/guice-throwingproviders/4.0/guice-throwingproviders-4.0.pom",
+      "sha1": "5118433baea2efed034af00a96e324b5717e8059"
     },
     {
-      "path": "com/google/inject/guice-parent/4.0-beta5/guice-parent-4.0-beta5.pom",
-      "sha1": "13d7df2b77236548d1e7cb9ba688686ddd4f19a5"
+      "path": "com/google/inject/guice-parent/4.0/guice-parent-4.0.pom",
+      "sha1": "a59ca1d3d70552158088d7f71e6c7e8779b9a8a1"
     },
     {
-      "path": "com/google/inject/guice/4.0-beta5/guice-4.0-beta5-no_aop.jar",
-      "sha1": "7706f581d709b1afd89b4e0dbf1bebf250abbd9b"
+      "path": "com/google/inject/guice/4.0/guice-4.0-no_aop.jar",
+      "sha1": "199b7acaa05b570bbccf31be998f013963e5e752"
     },
     {
-      "path": "com/google/inject/guice/4.0-beta5/guice-4.0-beta5.pom",
-      "sha1": "1e968b8c1da8cb48b7c0b77ffc565f92f313c392"
+      "path": "com/google/inject/guice/4.0/guice-4.0.pom",
+      "sha1": "688cb7b0d86456e3706573fe583173ee5e728f4e"
     },
     {
       "path": "com/google/j2objc/j2objc-annotations/1.3/j2objc-annotations-1.3.jar",