Disable SimpleSub by default, but enable it in ktest.mak and ktest-fa…

…il.mak for testing.
runtimeverification · Dec 1, 2023 · cef8679 · cef8679
1 parent b1965f7
commit cef8679
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
+KOMPILE_FLAGS+=--no-exc-wrap --type-inference-mode simplesub
 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
+KOMPILE_FLAGS+=--no-exc-wrap --type-inference-mode simplesub
 KPROVE_FLAGS+=--no-exc-wrap
 KRUN_FLAGS+=--no-exc-wrap
 

diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java
@@ -257,5 +257,5 @@ public enum TypeInferenceMode {
           "Choose between the Z3-based and SimpleSub-based type inference algorithms, or run both"
               + " and check that their results are equal. Must be one of [z3|simplesub|checked].",
       hidden = true)
-  public TypeInferenceMode typeInferenceMode = TypeInferenceMode.SIMPLESUB;
+  public TypeInferenceMode typeInferenceMode = TypeInferenceMode.Z3;
 }