Temporarily re-enable CHECKED to ensure CI still passes

runtimeverification · Dec 2, 2023 · 536db01 · 536db01
1 parent bbde842
commit 536db01
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/k-distribution/include/kframework/ktest-fail.mak b/k-distribution/include/kframework/ktest-fail.mak
@@ -14,7 +14,7 @@ TESTS?=$(wildcard $(DEFDIR)/*.md) $(wildcard $(DEFDIR)/*.k)
 KOMPILE_BACKEND?=llvm
 KAST_TESTS?=$(wildcard ./*.kast)
 
-KOMPILE_FLAGS+=--no-exc-wrap --type-inference-mode simplesub
+KOMPILE_FLAGS+=--no-exc-wrap --type-inference-mode checked
 KPROVE_FLAGS+=--no-exc-wrap
 KRUN_FLAGS+=--no-exc-wrap
 

diff --git a/k-distribution/include/kframework/ktest.mak b/k-distribution/include/kframework/ktest.mak
@@ -52,7 +52,7 @@ ifeq ($(UNAME), Darwin)
 	KOMPILE_FLAGS+=--no-haskell-binary
 endif
 
-KOMPILE_FLAGS+=--no-exc-wrap --type-inference-mode simplesub
+KOMPILE_FLAGS+=--no-exc-wrap --type-inference-mode checked
 KPROVE_FLAGS+=--no-exc-wrap
 KRUN_FLAGS+=--no-exc-wrap
 

diff --git a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java
@@ -142,7 +142,7 @@ private ParseInModule(
     this.typeInferenceDebug = typeInferenceDebug;
     this.typeInferenceMode =
         typeInferenceMode == KompileOptions.TypeInferenceMode.DEFAULT
-            ? KompileOptions.TypeInferenceMode.Z3
+            ? KompileOptions.TypeInferenceMode.CHECKED
             : typeInferenceMode;
     this.partialParseDebug = partialParseDebug;
   }