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/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 2aaa084b516..86402c537c6 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/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/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/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",