[feat] Set Z3 solver as default

UnitTestBot · Jul 22, 2023 · 2c4da76 · 2c4da76
1 parent 5b11579
commit 2c4da76
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 17 deletions.
diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
@@ -21,6 +21,7 @@ env:
   LLVM_VERSION: 11
   MINISAT_VERSION: "master"
   REQUIRES_RTTI: 0
+  SOLVERS: Z3:STP
   STP_VERSION: 2.3.3
   TCMALLOC_VERSION: 2.9.1
   UCLIBC_VERSION: klee_uclibc_v1.3
@@ -55,43 +56,35 @@ jobs:
           - name: "LLVM 14"
             env:
               LLVM_VERSION: 14
-              SOLVERS: Z3
           - name: "LLVM 13"
             env:
               LLVM_VERSION: 13
-              SOLVERS: Z3
           - name: "LLVM 12"
             env:
               LLVM_VERSION: 12
-              SOLVERS: Z3
           - name: "LLVM 11, Doxygen"
             env:
               LLVM_VERSION: 11
               ENABLE_DOXYGEN: 1
-              SOLVERS: Z3
           - name: "LLVM 10"
             env:
               LLVM_VERSION: 10
-              SOLVERS: Z3
           - name: "LLVM 9"
             env:
               LLVM_VERSION: 9
-              SOLVERS: Z3
           # Sanitizer builds. Do unoptimized build otherwise the optimizer
           # might remove problematic code
           - name: "ASan"
             env:
               SANITIZER_BUILD: address
               ENABLE_OPTIMIZED: 0
               USE_TCMALLOC: 0
-              SOLVERS: STP
               SANITIZER_LLVM_VERSION: 12
           - name: "UBSan"
             env:
               SANITIZER_BUILD: undefined
               ENABLE_OPTIMIZED: 0
               USE_TCMALLOC: 0
-              SOLVERS: STP
               SANITIZER_LLVM_VERSION: 12
           - name: "MSan"
             env:
@@ -119,12 +112,10 @@ jobs:
           # Check we can build latest klee-uclibc branch
           - name: "Latest klee-uclibc"
             env:
-              SOLVERS: Z3
               UCLIBC_VERSION: klee_0_9_29
           # Check at least one build with Asserts disabled.
           - name: "Asserts disabled"
             env:
-              SOLVERS: STP
               DISABLE_ASSERTIONS: 1
           # Check without TCMALLOC and with an optimised runtime library
           - name: "No TCMalloc, optimised runtime"
@@ -188,7 +179,7 @@ jobs:
               SOLVERS: STP
           - name: "Z3"
             env:
-              SOLVERS: Z3
+              SOLVERS: Z3:STP
     env:
       ENABLE_OPTIMIZED: 0
       COVERAGE: 1

diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp
@@ -174,16 +174,16 @@ cl::opt<klee::MetaSMTBackendType> MetaSMTBackend(
 #endif /* ENABLE_METASMT */
 
 // Pick the default core solver based on configuration
-#ifdef ENABLE_STP
-#define STP_IS_DEFAULT_STR " (default)"
-#define METASMT_IS_DEFAULT_STR ""
-#define Z3_IS_DEFAULT_STR ""
-#define DEFAULT_CORE_SOLVER STP_SOLVER
-#elif ENABLE_Z3
+#ifdef ENABLE_Z3
 #define STP_IS_DEFAULT_STR ""
 #define METASMT_IS_DEFAULT_STR ""
 #define Z3_IS_DEFAULT_STR " (default)"
 #define DEFAULT_CORE_SOLVER Z3_SOLVER
+#elif ENABLE_STP
+#define STP_IS_DEFAULT_STR " (default)"
+#define METASMT_IS_DEFAULT_STR ""
+#define Z3_IS_DEFAULT_STR ""
+#define DEFAULT_CORE_SOLVER STP_SOLVER
 #elif ENABLE_METASMT
 #define STP_IS_DEFAULT_STR ""
 #define METASMT_IS_DEFAULT_STR " (default)"

diff --git a/test/ArrayOpt/test_nier.c b/test/ArrayOpt/test_nier.c
@@ -1,3 +1,4 @@
+// REQUIRES: not-asan
 // REQUIRES: not-msan
 // Ignore msan: Generates a large stack trace > 8k but not a stack overflow for larger stacks
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc