diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index e1b4cde6f8..9b7667ee62 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -121,7 +121,8 @@ ExecutionState::ExecutionState()
       depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0),
       steppedMemoryInstructions(0), instsSinceCovNew(0),
       roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew({}),
-      forkDisabled(false), prevHistory_(TargetsHistory::create()),
+      coveredNewError(new box<bool>(false)), forkDisabled(false),
+      prevHistory_(TargetsHistory::create()),
       history_(TargetsHistory::create()) {
   setID();
 }
@@ -131,7 +132,8 @@ ExecutionState::ExecutionState(KFunction *kf)
       depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0),
       steppedMemoryInstructions(0), instsSinceCovNew(0),
       roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew({}),
-      forkDisabled(false), prevHistory_(TargetsHistory::create()),
+      coveredNewError(new box<bool>(false)), forkDisabled(false),
+      prevHistory_(TargetsHistory::create()),
       history_(TargetsHistory::create()) {
   pushFrame(nullptr, kf);
   setID();
@@ -142,7 +144,8 @@ ExecutionState::ExecutionState(KFunction *kf, KBlock *kb)
       depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0),
       steppedMemoryInstructions(0), instsSinceCovNew(0),
       roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew({}),
-      forkDisabled(false), prevHistory_(TargetsHistory::create()),
+      coveredNewError(new box<bool>(false)), forkDisabled(false),
+      prevHistory_(TargetsHistory::create()),
       history_(TargetsHistory::create()) {
   pushFrame(nullptr, kf);
   setID();
@@ -170,11 +173,11 @@ ExecutionState::ExecutionState(const ExecutionState &state)
       unwindingInformation(state.unwindingInformation
                                ? state.unwindingInformation->clone()
                                : nullptr),
-      coveredNew(state.coveredNew), forkDisabled(state.forkDisabled),
-      returnValue(state.returnValue), gepExprBases(state.gepExprBases),
-      prevTargets_(state.prevTargets_), targets_(state.targets_),
-      prevHistory_(state.prevHistory_), history_(state.history_),
-      isTargeted_(state.isTargeted_) {
+      coveredNew(state.coveredNew), coveredNewError(state.coveredNewError),
+      forkDisabled(state.forkDisabled), returnValue(state.returnValue),
+      gepExprBases(state.gepExprBases), prevTargets_(state.prevTargets_),
+      targets_(state.targets_), prevHistory_(state.prevHistory_),
+      history_(state.history_), isTargeted_(state.isTargeted_) {
   queryMetaData.id = state.id;
 }
 
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index f8cc093489..9492e1ce02 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -366,6 +366,7 @@ class ExecutionState {
 
   /// @brief Whether a new instruction was covered in this state
   mutable std::deque<ref<box<bool>>> coveredNew;
+  mutable ref<box<bool>> coveredNewError;
 
   /// @brief Disables forking for this state. Set by user code
   bool forkDisabled = false;
@@ -507,7 +508,12 @@ class ExecutionState {
   bool isCoveredNew() const {
     return !coveredNew.empty() && coveredNew.back()->value;
   }
-  void coverNew() const { coveredNew.push_back(new box<bool>(true)); }
+  bool isCoveredNewError() const { return coveredNewError->value; }
+  void coverNew() const {
+    coveredNew.push_back(new box<bool>(true));
+    coveredNewError->value = false;
+    coveredNewError = new box<bool>(true);
+  }
   void updateCoveredNew() const {
     while (!coveredNew.empty() && !coveredNew.front()->value) {
       coveredNew.pop_front();
@@ -519,6 +525,7 @@ class ExecutionState {
     }
     coveredNew.clear();
   }
+  void clearCoveredNewError() const { coveredNewError->value = false; }
 };
 
 struct ExecutionStateIDCompare {
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index e3c8cce344..e30001d601 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -4355,9 +4355,9 @@ void Executor::initializeTypeManager() {
   typeSystemManager->initModule();
 }
 
-static bool shouldWriteTest(const ExecutionState &state) {
+static bool shouldWriteTest(const ExecutionState &state, bool isError = false) {
   state.updateCoveredNew();
-  bool coveredNew = state.isCoveredNew();
+  bool coveredNew = isError ? state.isCoveredNewError() : state.isCoveredNew();
   return !OnlyOutputStatesCoveringNew || coveredNew;
 }
 
@@ -4721,7 +4721,7 @@ void Executor::terminateStateOnError(ExecutionState &state,
 
   if ((EmitAllErrors ||
        emittedErrors.insert(std::make_pair(lastInst, message)).second) &&
-      shouldWriteTest(state)) {
+      shouldWriteTest(state, true)) {
     std::string filepath = ki->getSourceFilepath();
     if (!filepath.empty()) {
       klee_message("ERROR: %s:%zu: %s", filepath.c_str(), ki->getLine(),
@@ -4752,6 +4752,8 @@ void Executor::terminateStateOnError(ExecutionState &state,
     if (!info_str.empty())
       msg << "Info: \n" << info_str;
 
+    state.clearCoveredNewError();
+
     const std::string ext = terminationTypeFileExtension(terminationType);
     // use user provided suffix from klee_report_error()
     const char *file_suffix = suffix ? suffix : ext.c_str();
diff --git a/test/Feature/LazyInitialization/DerefSymbolicPointer.c b/test/Feature/LazyInitialization/DerefSymbolicPointer.c
index 27fd4d1d42..b0919d56a3 100644
--- a/test/Feature/LazyInitialization/DerefSymbolicPointer.c
+++ b/test/Feature/LazyInitialization/DerefSymbolicPointer.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --write-kqueries --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects %t.bc > %t.log
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --skip-not-symbolic-objects %t.bc > %t.log
 // RUN: FileCheck %s -input-file=%t.log
 #include "klee/klee.h"
 
diff --git a/test/Feature/LazyInitialization/ImpossibleAddressForLI.c b/test/Feature/LazyInitialization/ImpossibleAddressForLI.c
index abc643eb05..f0d9f25bf6 100644
--- a/test/Feature/LazyInitialization/ImpossibleAddressForLI.c
+++ b/test/Feature/LazyInitialization/ImpossibleAddressForLI.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects %t.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/LazyInitialization/LazyInitialization.c b/test/Feature/LazyInitialization/LazyInitialization.c
index 74356f31b3..31e82a124e 100644
--- a/test/Feature/LazyInitialization/LazyInitialization.c
+++ b/test/Feature/LazyInitialization/LazyInitialization.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects --use-timestamps=false --use-guided-search=none %t.bc > %t.log
+// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects --use-timestamps=false --use-guided-search=none %t.bc > %t.log
 // RUN: FileCheck %s -input-file=%t.log
 
 struct Node {
diff --git a/test/Feature/LazyInitialization/LinkedList.c b/test/Feature/LazyInitialization/LinkedList.c
index 9431e4ffc3..191ce3103b 100644
--- a/test/Feature/LazyInitialization/LinkedList.c
+++ b/test/Feature/LazyInitialization/LinkedList.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --write-kqueries --solver-backend=z3 --output-dir=%t.klee-out --skip-not-symbolic-objects %t.bc > %t.log
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --skip-not-symbolic-objects %t.bc > %t.log
 // RUN: FileCheck %s -input-file=%t.log
 #include "klee/klee.h"
 
diff --git a/test/Feature/LazyInitialization/PointerOffset.c b/test/Feature/LazyInitialization/PointerOffset.c
index aaf3694e1c..2d0b7a4321 100644
--- a/test/Feature/LazyInitialization/PointerOffset.c
+++ b/test/Feature/LazyInitialization/PointerOffset.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects --use-timestamps=false --skip-local=false %t.bc
+// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects --use-timestamps=false --skip-local=false %t.bc
 // RUN: %ktest-tool %t.klee-out/test*.ktest > %t.log
 // RUN: FileCheck %s -input-file=%t.log
 // CHECK: pointers: [(0, 1, 4)]
diff --git a/test/Feature/LazyInitialization/SingleInitializationAndAccess.c b/test/Feature/LazyInitialization/SingleInitializationAndAccess.c
index 1def3a9876..4c2413aa9e 100644
--- a/test/Feature/LazyInitialization/SingleInitializationAndAccess.c
+++ b/test/Feature/LazyInitialization/SingleInitializationAndAccess.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects --skip-local=false --use-sym-size-li --min-number-elements-li=1 %t1.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects --skip-local=false --use-sym-size-li --min-number-elements-li=1 %t1.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 #include <assert.h>
diff --git a/test/Feature/LazyInitialization/TwoObjectsInitialization.c b/test/Feature/LazyInitialization/TwoObjectsInitialization.c
index ab67462f3d..957f4bd7da 100644
--- a/test/Feature/LazyInitialization/TwoObjectsInitialization.c
+++ b/test/Feature/LazyInitialization/TwoObjectsInitialization.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects %t1.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects %t1.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 #include <assert.h>
diff --git a/test/Industry/AssignNull_Scene_BadCase02.c b/test/Industry/AssignNull_Scene_BadCase02.c
index ecb898b0b2..55fb4b7989 100644
--- a/test/Industry/AssignNull_Scene_BadCase02.c
+++ b/test/Industry/AssignNull_Scene_BadCase02.c
@@ -49,7 +49,6 @@ void TestBad5(struct STU *pdev, const char *buf, unsigned int count)
     printf("teacher id is %ud", teacherID);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --location-accuracy --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/AssignNull_Scene_BadCase04.c b/test/Industry/AssignNull_Scene_BadCase04.c
index 757479e40d..6a0979278f 100644
--- a/test/Industry/AssignNull_Scene_BadCase04.c
+++ b/test/Industry/AssignNull_Scene_BadCase04.c
@@ -50,7 +50,6 @@ int TestBad7(char *arg, unsigned int count)
     return 1;
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --smart-resolve-entry-function --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/BadCase01_SecB_ForwardNull.c b/test/Industry/BadCase01_SecB_ForwardNull.c
index 38431719b3..f72959d73c 100644
--- a/test/Industry/BadCase01_SecB_ForwardNull.c
+++ b/test/Industry/BadCase01_SecB_ForwardNull.c
@@ -140,7 +140,6 @@ void badbad(char *ptr)
 }
 #endif
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/CheckNull_Scene_BadCase02.c b/test/Industry/CheckNull_Scene_BadCase02.c
index fc27954a53..3effb46f57 100644
--- a/test/Industry/CheckNull_Scene_BadCase02.c
+++ b/test/Industry/CheckNull_Scene_BadCase02.c
@@ -41,7 +41,6 @@ void TestBad2()
     free(errMsg);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/CheckNull_Scene_BadCase04.c b/test/Industry/CheckNull_Scene_BadCase04.c
index dba74dd82a..0e9038201d 100644
--- a/test/Industry/CheckNull_Scene_BadCase04.c
+++ b/test/Industry/CheckNull_Scene_BadCase04.c
@@ -56,7 +56,6 @@ void TestBad12(int cond1, int cond2)
 	}
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/FN_SecB_ForwardNull_filed.c b/test/Industry/FN_SecB_ForwardNull_filed.c
index fad10a2644..6faaf136b9 100644
--- a/test/Industry/FN_SecB_ForwardNull_filed.c
+++ b/test/Industry/FN_SecB_ForwardNull_filed.c
@@ -1,8 +1,3 @@
-// REQUIRES: z3
-// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
-// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
 /*
  * Copyright (c) Huawei Technologies Co., Ltd. 2021-2021. All rights reserved.
  * @description 空指针解引用 验收失败
@@ -44,8 +39,13 @@ void WB_BadCase_Field(UINT32 inputNum1, UINT32 inputNum2)
 void WB_BadCase_field2(DataInfo *data)
 {
   data->dataBuff = NULL;
-  *data->dataBuff = 'c'; // CHECK: KLEE: WARNING: 100.00% NullPointerException False Negative at: {{.*}}test/Industry/FN_SecB_ForwardNull_filed.c:47 19
+  *data->dataBuff = 'c'; // CHECK: KLEE: WARNING: 100.00% NullPointerException False Negative at: {{.*}}test/Industry/FN_SecB_ForwardNull_filed.c:42 19
 
   char *ptr = NULL;
   *ptr = 'c'; // CHECK: KLEE: WARNING: 100.00% NullPointerException False Positive at trace 1
 }
+
+// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
\ No newline at end of file
diff --git a/test/Industry/FN_SecB_ForwardNull_filed.c.json b/test/Industry/FN_SecB_ForwardNull_filed.c.json
index b54baa91f9..ec0f7d3101 100644
--- a/test/Industry/FN_SecB_ForwardNull_filed.c.json
+++ b/test/Industry/FN_SecB_ForwardNull_filed.c.json
@@ -20,7 +20,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/forward_null/./FN_SecB_ForwardNull_filed.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 49,
+                                                        "startLine": 44,
                                                         "startColumn": null
                                                     }
                                                 }
@@ -33,7 +33,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/forward_null/./FN_SecB_ForwardNull_filed.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 50,
+                                                        "startLine": 45,
                                                         "startColumn": null
                                                     }
                                                 }
@@ -52,7 +52,7 @@
                                     "uri": "/mnt/d/wsl-ubuntu/test2/forward_null/./FN_SecB_ForwardNull_filed.c"
                                 },
                                 "region": {
-                                    "startLine": 50,
+                                    "startLine": 45,
                                     "startColumn": null
                                 }
                             }
diff --git a/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c b/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c
index 4b77bd1b66..9a04367627 100644
--- a/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c
+++ b/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c
@@ -53,7 +53,6 @@ void call_func(int num)
     ResourceLeak_bad01(num);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --write-kqueries --max-cycles-before-stuck=0 --use-guided-search=error --check-out-of-memory --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/NullReturn_BadCase_WhiteBox01.c b/test/Industry/NullReturn_BadCase_WhiteBox01.c
index 8ee8261adb..666c470216 100644
--- a/test/Industry/NullReturn_BadCase_WhiteBox01.c
+++ b/test/Industry/NullReturn_BadCase_WhiteBox01.c
@@ -1,8 +1,3 @@
-// REQUIRES: z3
-// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --smart-resolve-entry-function --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
-// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
 /*
  * Copyright (c) Huawei Technologies Co., Ltd. 2022-2022. All rights reserved.
  *
@@ -68,3 +63,8 @@ void NullReturn_BadCase_WhiteBox01(UINT8 index, SchedHarqStru *harqInfo)
         SendMsg(index, usrId, resultInfo);                                                              // (3)
     }
 }
+
+// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --smart-resolve-entry-function --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
\ No newline at end of file
diff --git a/test/Industry/NullReturn_BadCase_WhiteBox01.c.json b/test/Industry/NullReturn_BadCase_WhiteBox01.c.json
index 3372239023..42a4b510f1 100644
--- a/test/Industry/NullReturn_BadCase_WhiteBox01.c.json
+++ b/test/Industry/NullReturn_BadCase_WhiteBox01.c.json
@@ -20,7 +20,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 45,
+                                                        "startLine": 40,
                                                         "startColumn": 9
                                                     }
                                                 }
@@ -33,7 +33,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 66,
+                                                        "startLine": 61,
                                                         "startColumn": 34
                                                     }
                                                 }
@@ -46,7 +46,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 68,
+                                                        "startLine": 63,
                                                         "startColumn": 9
                                                     }
                                                 }
@@ -59,7 +59,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 56,
+                                                        "startLine": 51,
                                                         "startColumn": 30
                                                     }
                                                 }
@@ -78,7 +78,7 @@
                                     "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                 },
                                 "region": {
-                                    "startLine": 56,
+                                    "startLine": 51,
                                     "startColumn": 30
                                 }
                             }
@@ -98,7 +98,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 45,
+                                                        "startLine": 40,
                                                         "startColumn": 9
                                                     }
                                                 }
@@ -111,7 +111,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 66,
+                                                        "startLine": 61,
                                                         "startColumn": 34
                                                     }
                                                 }
@@ -124,7 +124,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 68,
+                                                        "startLine": 63,
                                                         "startColumn": 9
                                                     }
                                                 }
@@ -137,7 +137,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 54,
+                                                        "startLine": 49,
                                                         "startColumn": 30
                                                     }
                                                 }
@@ -156,7 +156,7 @@
                                     "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                 },
                                 "region": {
-                                    "startLine": 54,
+                                    "startLine": 49,
                                     "startColumn": 30
                                 }
                             }
diff --git a/test/Industry/NullReturn_Scene_BadCase01.c b/test/Industry/NullReturn_Scene_BadCase01.c
index cfab0db844..45b8240318 100644
--- a/test/Industry/NullReturn_Scene_BadCase01.c
+++ b/test/Industry/NullReturn_Scene_BadCase01.c
@@ -39,7 +39,6 @@ void TestBad1()
     free(buf);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --external-calls=all --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/NullReturn_Scene_BadCase02.c b/test/Industry/NullReturn_Scene_BadCase02.c
index 7042eb01b1..d25af79653 100644
--- a/test/Industry/NullReturn_Scene_BadCase02.c
+++ b/test/Industry/NullReturn_Scene_BadCase02.c
@@ -38,7 +38,6 @@ void TestBad2()
     printf("The second is %d", info->tm_sec); // CHECK: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --location-accuracy --mock-external-calls --check-out-of-memory --skip-not-symbolic-objects --skip-not-lazy-initialized --extern-calls-can-return-null --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/NullReturn_Scene_BadCase03.c b/test/Industry/NullReturn_Scene_BadCase03.c
index f24ef754b6..c4190f9bb2 100644
--- a/test/Industry/NullReturn_Scene_BadCase03.c
+++ b/test/Industry/NullReturn_Scene_BadCase03.c
@@ -40,7 +40,6 @@ void TestBad3()
     free(buf);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/NullReturn_Scene_BadCase04.c b/test/Industry/NullReturn_Scene_BadCase04.c
index d7054e5af2..377e4b9e19 100644
--- a/test/Industry/NullReturn_Scene_BadCase04.c
+++ b/test/Industry/NullReturn_Scene_BadCase04.c
@@ -44,7 +44,6 @@ void TestBad4()
     free(buf);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --check-out-of-memory --mock-external-calls --libc=klee --external-calls=all --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/NullReturn_Scene_BadCase06.c b/test/Industry/NullReturn_Scene_BadCase06.c
index 8ad07ac540..19b11d341b 100644
--- a/test/Industry/NullReturn_Scene_BadCase06.c
+++ b/test/Industry/NullReturn_Scene_BadCase06.c
@@ -52,7 +52,6 @@ void TestBad6(unsigned int count)
     free(buf);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/NullReturn_Scene_BadCase08.cpp b/test/Industry/NullReturn_Scene_BadCase08.cpp
index 07870565a0..91e6dccdf8 100644
--- a/test/Industry/NullReturn_Scene_BadCase08.cpp
+++ b/test/Industry/NullReturn_Scene_BadCase08.cpp
@@ -37,7 +37,6 @@ void TestBad9()
 	printf("the current integer is: %d", *p); // CHECK: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1
 }
 
-// REQUIRES: z3
 // RUN: %clangxx %s -emit-llvm %O0opt -c -g -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --write-kqueries --use-guided-search=error --location-accuracy --mock-external-calls --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/SecB_ForwardNull.c b/test/Industry/SecB_ForwardNull.c
index ef5866afbc..e3a8334c82 100644
--- a/test/Industry/SecB_ForwardNull.c
+++ b/test/Industry/SecB_ForwardNull.c
@@ -1,8 +1,3 @@
-// REQUIRES: z3
-// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
-// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
 /*
  * Copyright (c) Huawei Technologies Co., Ltd. 2021-2021. All rights reserved.
  * @description 空指针解引用 验收失败
@@ -133,3 +128,8 @@ void badbad(char *ptr)
   ptr = NULL;
   *ptr = 'a'; // CHECK: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1
 }
+
+// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
\ No newline at end of file
diff --git a/test/Industry/SecB_ForwardNull.c.json b/test/Industry/SecB_ForwardNull.c.json
index d26344534b..ee8294c266 100644
--- a/test/Industry/SecB_ForwardNull.c.json
+++ b/test/Industry/SecB_ForwardNull.c.json
@@ -20,7 +20,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/forward_null/SecB_ForwardNull.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 133,
+                                                        "startLine": 128,
                                                         "startColumn": null
                                                     }
                                                 }
@@ -33,7 +33,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/forward_null/SecB_ForwardNull.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 134,
+                                                        "startLine": 129,
                                                         "startColumn": null
                                                     }
                                                 }
@@ -52,7 +52,7 @@
                                     "uri": "/mnt/d/wsl-ubuntu/test2/forward_null/SecB_ForwardNull.c"
                                 },
                                 "region": {
-                                    "startLine": 134,
+                                    "startLine": 129,
                                     "startColumn": null
                                 }
                             }
diff --git a/test/Industry/UseAfterFree/Double_Free_BadCase01.c b/test/Industry/UseAfterFree/Double_Free_BadCase01.c
index cece04e8a7..57d3600faa 100644
--- a/test/Industry/UseAfterFree/Double_Free_BadCase01.c
+++ b/test/Industry/UseAfterFree/Double_Free_BadCase01.c
@@ -16,8 +16,8 @@
  * @author xwx356597;x00407107
  * 
  */
+
 #include <stdio.h>
-#include <malloc.h>
 
 //@scene 指针释放后未置空导致双重释放
 void DoubleFreeBad01()
@@ -36,7 +36,6 @@ void DoubleFreeBad01()
     free(p); // CHECK: KLEE: WARNING: 100.00% DoubleFree True Positive at trace 1
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/UseAfterFree/Double_Free_BadCase02.c b/test/Industry/UseAfterFree/Double_Free_BadCase02.c
index e6e93818d8..be8f1c52c1 100644
--- a/test/Industry/UseAfterFree/Double_Free_BadCase02.c
+++ b/test/Industry/UseAfterFree/Double_Free_BadCase02.c
@@ -16,8 +16,8 @@
  * @author xwx356597;x00407107
  * 
  */
+
 #include <stdio.h>
-#include <malloc.h>
 
 //@scene 指针释放后未置空，有条件地再再次释放导致双重释放
 void DoubleFreeBad02(int flag)
@@ -39,7 +39,6 @@ void DoubleFreeBad02(int flag)
     }
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/UseAfterFree/Free_Not_Set_Null_BadCase02.cpp b/test/Industry/UseAfterFree/Free_Not_Set_Null_BadCase02.cpp
index 6c15434bf4..90a32d9903 100644
--- a/test/Industry/UseAfterFree/Free_Not_Set_Null_BadCase02.cpp
+++ b/test/Industry/UseAfterFree/Free_Not_Set_Null_BadCase02.cpp
@@ -17,7 +17,6 @@
  *
  */
 
-#include <malloc.h>
 #include <stdlib.h>
 #include <stdio.h>
 
@@ -34,6 +33,7 @@ typedef struct {
     int a;
     char *pname;
 }Data;
+
 //全局变量 分支结束前要重新赋值
 char *MSG = (char*)malloc(1000);
 
@@ -75,7 +75,6 @@ int main()
     return 0;
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/UseAfterFree/Prod_Dereference_After_Free_BadCase01.c b/test/Industry/UseAfterFree/Prod_Dereference_After_Free_BadCase01.c
index 9c171549e9..7742d31afd 100644
--- a/test/Industry/UseAfterFree/Prod_Dereference_After_Free_BadCase01.c
+++ b/test/Industry/UseAfterFree/Prod_Dereference_After_Free_BadCase01.c
@@ -33,7 +33,6 @@ void UseAfterFree()
     return;
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/ZeroDeref_Scene_BadCase02.c b/test/Industry/ZeroDeref_Scene_BadCase02.c
index 0e65b66155..dd0fe063ac 100644
--- a/test/Industry/ZeroDeref_Scene_BadCase02.c
+++ b/test/Industry/ZeroDeref_Scene_BadCase02.c
@@ -38,7 +38,6 @@ void TestBad9()
     memcpy(pDest, p, BUFFERSIZE); // CHECK-DAG: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/ZeroDeref_Scene_BadCase05.c b/test/Industry/ZeroDeref_Scene_BadCase05.c
index d094cea77b..3afb67837e 100644
--- a/test/Industry/ZeroDeref_Scene_BadCase05.c
+++ b/test/Industry/ZeroDeref_Scene_BadCase05.c
@@ -62,7 +62,6 @@ void TestBad18(struct STU *stu)
 	HelpBadTest1(NULL);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --check-out-of-memory --mock-external-calls --libc=klee --external-calls=all --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/fn_reverse_null.c b/test/Industry/fn_reverse_null.c
index 0e02ebc842..aff52b8f68 100644
--- a/test/Industry/fn_reverse_null.c
+++ b/test/Industry/fn_reverse_null.c
@@ -53,7 +53,6 @@ void TestErr4(TreeNode *head)
     return;
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --external-calls=all --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/fp_forward_null_address.c b/test/Industry/fp_forward_null_address.c
index f39297d2a4..e090051722 100644
--- a/test/Industry/fp_forward_null_address.c
+++ b/test/Industry/fp_forward_null_address.c
@@ -22,7 +22,6 @@ void foo()
   int v = *p; // CHECK: KLEE: WARNING: 100.00% NullPointerException False Positive at trace 1
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --max-cycles-before-stuck=150 --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/fp_null_returns_self_define.c b/test/Industry/fp_null_returns_self_define.c
index 2ed62cfb68..fa331108b6 100644
--- a/test/Industry/fp_null_returns_self_define.c
+++ b/test/Industry/fp_null_returns_self_define.c
@@ -1,4 +1,3 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/fp_null_returns_self_define2.c b/test/Industry/fp_null_returns_self_define2.c
index f737f18cc5..6606140676 100644
--- a/test/Industry/fp_null_returns_self_define2.c
+++ b/test/Industry/fp_null_returns_self_define2.c
@@ -26,7 +26,6 @@ void TEST_NullReturns004(unsigned short index)
     sink(value);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/if2.c b/test/Industry/if2.c
index d52edf529f..e41a4a0a0e 100644
--- a/test/Industry/if2.c
+++ b/test/Industry/if2.c
@@ -8,7 +8,6 @@ int main(int x) {
   return *p;
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --search=bfs --max-stepped-instructions=20 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/test.c b/test/Industry/test.c
index 9d84770da0..5b08e0cd97 100644
--- a/test/Industry/test.c
+++ b/test/Industry/test.c
@@ -19,7 +19,6 @@ void TestBad8(int len)
         buf[0] = 'a'; // CHECK-NUM: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1
 }                     // CHECK-UID: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 8389b1896658d867c9e15267acfe8c32
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/while_true.c b/test/Industry/while_true.c
index a2eebdcc0a..f0566cce12 100644
--- a/test/Industry/while_true.c
+++ b/test/Industry/while_true.c
@@ -8,7 +8,6 @@ int main() {
   return *p;
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out-1
 // RUN: %klee --output-dir=%t.klee-out-1 --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=10 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
diff --git a/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c b/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c
index 7a6d4ff09c..6048923249 100644
--- a/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c
+++ b/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c
@@ -1,7 +1,8 @@
-// REQUIRES: z3
+// REQUIRES: not-msan
+// Disabling msan because it times out on CI
 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false --solver-backend=z3 -max-memory=6008 --optimize=true --skip-not-lazy-initialized -output-source=true --output-stats=false --output-istats=false --write-xml-tests --write-ktests=false --xml-metadata-programfile=wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c --xml-metadata-programhash=a18daeacf63b42ad6e1cb490555b7cdecd71ad6e58b167ed0f5626c03bc3d772 --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --function-call-reproduce=reach_error --dump-states-on-halt=false -exit-on-error-type=Assert --search=dfs --search=random-path -max-time=20 %t1.bc 2>&1 | FileCheck -check-prefix=CHECK-VERDICT %s
+// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false -max-memory=6008 --optimize=true --skip-not-lazy-initialized -output-source=true --output-stats=false --output-istats=false --write-xml-tests --write-ktests=false --xml-metadata-programfile=wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c --xml-metadata-programhash=a18daeacf63b42ad6e1cb490555b7cdecd71ad6e58b167ed0f5626c03bc3d772 --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --function-call-reproduce=reach_error --dump-states-on-halt=false -exit-on-error-type=Assert --search=dfs --search=random-path -max-time=20 %t1.bc 2>&1 | FileCheck -check-prefix=CHECK-VERDICT %s
 
 // RUN: test -f %t.klee-out/test000001.xml
 // RUN: not test -f %t.klee-out/test000001.ktest
diff --git a/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c b/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c
index ec58f72187..66edca58dc 100644
--- a/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c
+++ b/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c
@@ -1,7 +1,7 @@
-// REQUIRES: not-darwin, z3
+// REQUIRES: not-darwin
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --libc=klee --posix-runtime --solver-backend=z3 --skip-not-lazy-initialized --skip-not-symbolic-objects %t.bc > %t.log
+// RUN: %klee --output-dir=%t.klee-out --libc=klee --posix-runtime --skip-not-lazy-initialized --skip-not-symbolic-objects %t.bc > %t.log
 
 // RUN: test -f %t.klee-out/test000006.ktest
 
diff --git a/test/regression/2023-10-04-email_spec0_product16.cil.c b/test/regression/2023-10-04-email_spec0_product16.cil.c
index 8a4acd5c58..e407b7bbb2 100644
--- a/test/regression/2023-10-04-email_spec0_product16.cil.c
+++ b/test/regression/2023-10-04-email_spec0_product16.cil.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang  -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false --solver-backend=z3 -max-memory=6008 --optimize --skip-not-lazy-initialized -istats-write-interval=90s -exit-on-error-type=Assert --search=dfs -max-time=10s %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s
+// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --istats-write-interval=90s --exit-on-error-type=Assert --search=dfs --max-time=10s %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s
 
 // RUN find %t.klee-out -type f -name "*.assert.err" | sed 's/assert\.err/ktest/' | xargs %ktest-tool | FileCheck -check-prefix=CHECK-TEST %s
 // CHECK-TEST-NOT: object 20
diff --git a/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c b/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c
index 9b27688a42..d08c61d74a 100644
--- a/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c
+++ b/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c
@@ -1,4 +1,3 @@
-// REQUIRES: z3
 // RUN: %clang  -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --optimize=true --delete-dead-loops=false --use-forked-solver=false -max-memory=6008 --cex-cache-validity-cores --only-output-states-covering-new=true --dump-states-on-halt=true %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s
diff --git a/test/regression/2023-10-06-Dubois-015.c b/test/regression/2023-10-06-Dubois-015.c
new file mode 100644
index 0000000000..fccb9acd93
--- /dev/null
+++ b/test/regression/2023-10-06-Dubois-015.c
@@ -0,0 +1,354 @@
+// RUN: %clang  -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=true --search=dfs %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s
+
+#include "klee-test-comp.c"
+
+// This file is part of the SV-Benchmarks collection of verification tasks:
+// https://github.com/sosy-lab/sv-benchmarks
+//
+// SPDX-FileCopyrightText: 2016 Gilles Audemard
+// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2020 The SV-Benchmarks Community
+//
+// SPDX-License-Identifier: MIT
+
+extern void abort(void) __attribute__((__nothrow__, __leaf__))
+__attribute__((__noreturn__));
+extern void __assert_fail(const char *, const char *, unsigned int,
+                          const char *) __attribute__((__nothrow__, __leaf__))
+__attribute__((__noreturn__));
+#ifdef GCOV
+extern void __gcov_dump(void);
+#endif
+
+void abort_prog() {
+#ifdef GCOV
+  __gcov_dump();
+#endif
+  abort();
+}
+int __VERIFIER_nondet_int();
+void reach_error() {
+  abort_prog();
+  __assert_fail("0", "Dubois-015.c", 5, "reach_error");
+}
+void assume(int cond) {
+  if (!cond)
+    abort_prog();
+}
+int main() {
+  int cond0;
+  int dummy = 0;
+  int N;
+  int var0;
+  var0 = __VERIFIER_nondet_int();
+  assume(var0 >= 0);
+  assume(var0 <= 1);
+  int var1;
+  var1 = __VERIFIER_nondet_int();
+  assume(var1 >= 0);
+  assume(var1 <= 1);
+  int var2;
+  var2 = __VERIFIER_nondet_int();
+  assume(var2 >= 0);
+  assume(var2 <= 1);
+  int var3;
+  var3 = __VERIFIER_nondet_int();
+  assume(var3 >= 0);
+  assume(var3 <= 1);
+  int var4;
+  var4 = __VERIFIER_nondet_int();
+  assume(var4 >= 0);
+  assume(var4 <= 1);
+  int var5;
+  var5 = __VERIFIER_nondet_int();
+  assume(var5 >= 0);
+  assume(var5 <= 1);
+  int var6;
+  var6 = __VERIFIER_nondet_int();
+  assume(var6 >= 0);
+  assume(var6 <= 1);
+  int var7;
+  var7 = __VERIFIER_nondet_int();
+  assume(var7 >= 0);
+  assume(var7 <= 1);
+  int var8;
+  var8 = __VERIFIER_nondet_int();
+  assume(var8 >= 0);
+  assume(var8 <= 1);
+  int var9;
+  var9 = __VERIFIER_nondet_int();
+  assume(var9 >= 0);
+  assume(var9 <= 1);
+  int var10;
+  var10 = __VERIFIER_nondet_int();
+  assume(var10 >= 0);
+  assume(var10 <= 1);
+  int var11;
+  var11 = __VERIFIER_nondet_int();
+  assume(var11 >= 0);
+  assume(var11 <= 1);
+  int var12;
+  var12 = __VERIFIER_nondet_int();
+  assume(var12 >= 0);
+  assume(var12 <= 1);
+  int var13;
+  var13 = __VERIFIER_nondet_int();
+  assume(var13 >= 0);
+  assume(var13 <= 1);
+  int var14;
+  var14 = __VERIFIER_nondet_int();
+  assume(var14 >= 0);
+  assume(var14 <= 1);
+  int var15;
+  var15 = __VERIFIER_nondet_int();
+  assume(var15 >= 0);
+  assume(var15 <= 1);
+  int var16;
+  var16 = __VERIFIER_nondet_int();
+  assume(var16 >= 0);
+  assume(var16 <= 1);
+  int var17;
+  var17 = __VERIFIER_nondet_int();
+  assume(var17 >= 0);
+  assume(var17 <= 1);
+  int var18;
+  var18 = __VERIFIER_nondet_int();
+  assume(var18 >= 0);
+  assume(var18 <= 1);
+  int var19;
+  var19 = __VERIFIER_nondet_int();
+  assume(var19 >= 0);
+  assume(var19 <= 1);
+  int var20;
+  var20 = __VERIFIER_nondet_int();
+  assume(var20 >= 0);
+  assume(var20 <= 1);
+  int var21;
+  var21 = __VERIFIER_nondet_int();
+  assume(var21 >= 0);
+  assume(var21 <= 1);
+  int var22;
+  var22 = __VERIFIER_nondet_int();
+  assume(var22 >= 0);
+  assume(var22 <= 1);
+  int var23;
+  var23 = __VERIFIER_nondet_int();
+  assume(var23 >= 0);
+  assume(var23 <= 1);
+  int var24;
+  var24 = __VERIFIER_nondet_int();
+  assume(var24 >= 0);
+  assume(var24 <= 1);
+  int var25;
+  var25 = __VERIFIER_nondet_int();
+  assume(var25 >= 0);
+  assume(var25 <= 1);
+  int var26;
+  var26 = __VERIFIER_nondet_int();
+  assume(var26 >= 0);
+  assume(var26 <= 1);
+  int var27;
+  var27 = __VERIFIER_nondet_int();
+  assume(var27 >= 0);
+  assume(var27 <= 1);
+  int var28;
+  var28 = __VERIFIER_nondet_int();
+  assume(var28 >= 0);
+  assume(var28 <= 1);
+  int var29;
+  var29 = __VERIFIER_nondet_int();
+  assume(var29 >= 0);
+  assume(var29 <= 1);
+  int var30;
+  var30 = __VERIFIER_nondet_int();
+  assume(var30 >= 0);
+  assume(var30 <= 1);
+  int var31;
+  var31 = __VERIFIER_nondet_int();
+  assume(var31 >= 0);
+  assume(var31 <= 1);
+  int var32;
+  var32 = __VERIFIER_nondet_int();
+  assume(var32 >= 0);
+  assume(var32 <= 1);
+  int var33;
+  var33 = __VERIFIER_nondet_int();
+  assume(var33 >= 0);
+  assume(var33 <= 1);
+  int var34;
+  var34 = __VERIFIER_nondet_int();
+  assume(var34 >= 0);
+  assume(var34 <= 1);
+  int var35;
+  var35 = __VERIFIER_nondet_int();
+  assume(var35 >= 0);
+  assume(var35 <= 1);
+  int var36;
+  var36 = __VERIFIER_nondet_int();
+  assume(var36 >= 0);
+  assume(var36 <= 1);
+  int var37;
+  var37 = __VERIFIER_nondet_int();
+  assume(var37 >= 0);
+  assume(var37 <= 1);
+  int var38;
+  var38 = __VERIFIER_nondet_int();
+  assume(var38 >= 0);
+  assume(var38 <= 1);
+  int var39;
+  var39 = __VERIFIER_nondet_int();
+  assume(var39 >= 0);
+  assume(var39 <= 1);
+  int var40;
+  var40 = __VERIFIER_nondet_int();
+  assume(var40 >= 0);
+  assume(var40 <= 1);
+  int var41;
+  var41 = __VERIFIER_nondet_int();
+  assume(var41 >= 0);
+  assume(var41 <= 1);
+  int var42;
+  var42 = __VERIFIER_nondet_int();
+  assume(var42 >= 0);
+  assume(var42 <= 1);
+  int var43;
+  var43 = __VERIFIER_nondet_int();
+  assume(var43 >= 0);
+  assume(var43 <= 1);
+  int var44;
+  var44 = __VERIFIER_nondet_int();
+  assume(var44 >= 0);
+  assume(var44 <= 1);
+  int myvar0 = 1;
+  assume((var28 == 0 & var29 == 0 & var0 == 1) |
+         (var28 == 0 & var29 == 1 & var0 == 0) |
+         (var28 == 1 & var29 == 0 & var0 == 0) |
+         (var28 == 1 & var29 == 1 & var0 == 1) | 0);
+  assume((var1 == 0 & var31 == 0 & var2 == 1) |
+         (var1 == 0 & var31 == 1 & var2 == 0) |
+         (var1 == 1 & var31 == 0 & var2 == 0) |
+         (var1 == 1 & var31 == 1 & var2 == 1) | 0);
+  assume((var2 == 0 & var32 == 0 & var3 == 1) |
+         (var2 == 0 & var32 == 1 & var3 == 0) |
+         (var2 == 1 & var32 == 0 & var3 == 0) |
+         (var2 == 1 & var32 == 1 & var3 == 1) | 0);
+  assume((var3 == 0 & var33 == 0 & var4 == 1) |
+         (var3 == 0 & var33 == 1 & var4 == 0) |
+         (var3 == 1 & var33 == 0 & var4 == 0) |
+         (var3 == 1 & var33 == 1 & var4 == 1) | 0);
+  assume((var4 == 0 & var34 == 0 & var5 == 1) |
+         (var4 == 0 & var34 == 1 & var5 == 0) |
+         (var4 == 1 & var34 == 0 & var5 == 0) |
+         (var4 == 1 & var34 == 1 & var5 == 1) | 0);
+  assume((var5 == 0 & var35 == 0 & var6 == 1) |
+         (var5 == 0 & var35 == 1 & var6 == 0) |
+         (var5 == 1 & var35 == 0 & var6 == 0) |
+         (var5 == 1 & var35 == 1 & var6 == 1) | 0);
+  assume((var6 == 0 & var36 == 0 & var7 == 1) |
+         (var6 == 0 & var36 == 1 & var7 == 0) |
+         (var6 == 1 & var36 == 0 & var7 == 0) |
+         (var6 == 1 & var36 == 1 & var7 == 1) | 0);
+  assume((var7 == 0 & var37 == 0 & var8 == 1) |
+         (var7 == 0 & var37 == 1 & var8 == 0) |
+         (var7 == 1 & var37 == 0 & var8 == 0) |
+         (var7 == 1 & var37 == 1 & var8 == 1) | 0);
+  assume((var8 == 0 & var38 == 0 & var9 == 1) |
+         (var8 == 0 & var38 == 1 & var9 == 0) |
+         (var8 == 1 & var38 == 0 & var9 == 0) |
+         (var8 == 1 & var38 == 1 & var9 == 1) | 0);
+  assume((var9 == 0 & var39 == 0 & var10 == 1) |
+         (var9 == 0 & var39 == 1 & var10 == 0) |
+         (var9 == 1 & var39 == 0 & var10 == 0) |
+         (var9 == 1 & var39 == 1 & var10 == 1) | 0);
+  assume((var10 == 0 & var40 == 0 & var11 == 1) |
+         (var10 == 0 & var40 == 1 & var11 == 0) |
+         (var10 == 1 & var40 == 0 & var11 == 0) |
+         (var10 == 1 & var40 == 1 & var11 == 1) | 0);
+  assume((var11 == 0 & var41 == 0 & var12 == 1) |
+         (var11 == 0 & var41 == 1 & var12 == 0) |
+         (var11 == 1 & var41 == 0 & var12 == 0) |
+         (var11 == 1 & var41 == 1 & var12 == 1) | 0);
+  assume((var12 == 0 & var42 == 0 & var13 == 1) |
+         (var12 == 0 & var42 == 1 & var13 == 0) |
+         (var12 == 1 & var42 == 0 & var13 == 0) |
+         (var12 == 1 & var42 == 1 & var13 == 1) | 0);
+  assume((var0 == 0 & var30 == 0 & var1 == 1) |
+         (var0 == 0 & var30 == 1 & var1 == 0) |
+         (var0 == 1 & var30 == 0 & var1 == 0) |
+         (var0 == 1 & var30 == 1 & var1 == 1) | 0);
+  assume((var14 == 0 & var43 == 0 & var44 == 1) |
+         (var14 == 0 & var43 == 1 & var44 == 0) |
+         (var14 == 1 & var43 == 0 & var44 == 0) |
+         (var14 == 1 & var43 == 1 & var44 == 1) | 0);
+  assume((var13 == 0 & var43 == 0 & var44 == 1) |
+         (var13 == 0 & var43 == 1 & var44 == 0) |
+         (var13 == 1 & var43 == 0 & var44 == 0) |
+         (var13 == 1 & var43 == 1 & var44 == 1) | 0);
+  assume((var16 == 0 & var41 == 0 & var15 == 1) |
+         (var16 == 0 & var41 == 1 & var15 == 0) |
+         (var16 == 1 & var41 == 0 & var15 == 0) |
+         (var16 == 1 & var41 == 1 & var15 == 1) | 0);
+  assume((var17 == 0 & var40 == 0 & var16 == 1) |
+         (var17 == 0 & var40 == 1 & var16 == 0) |
+         (var17 == 1 & var40 == 0 & var16 == 0) |
+         (var17 == 1 & var40 == 1 & var16 == 1) | 0);
+  assume((var18 == 0 & var39 == 0 & var17 == 1) |
+         (var18 == 0 & var39 == 1 & var17 == 0) |
+         (var18 == 1 & var39 == 0 & var17 == 0) |
+         (var18 == 1 & var39 == 1 & var17 == 1) | 0);
+  assume((var19 == 0 & var38 == 0 & var18 == 1) |
+         (var19 == 0 & var38 == 1 & var18 == 0) |
+         (var19 == 1 & var38 == 0 & var18 == 0) |
+         (var19 == 1 & var38 == 1 & var18 == 1) | 0);
+  assume((var20 == 0 & var37 == 0 & var19 == 1) |
+         (var20 == 0 & var37 == 1 & var19 == 0) |
+         (var20 == 1 & var37 == 0 & var19 == 0) |
+         (var20 == 1 & var37 == 1 & var19 == 1) | 0);
+  assume((var21 == 0 & var36 == 0 & var20 == 1) |
+         (var21 == 0 & var36 == 1 & var20 == 0) |
+         (var21 == 1 & var36 == 0 & var20 == 0) |
+         (var21 == 1 & var36 == 1 & var20 == 1) | 0);
+  assume((var22 == 0 & var35 == 0 & var21 == 1) |
+         (var22 == 0 & var35 == 1 & var21 == 0) |
+         (var22 == 1 & var35 == 0 & var21 == 0) |
+         (var22 == 1 & var35 == 1 & var21 == 1) | 0);
+  assume((var23 == 0 & var34 == 0 & var22 == 1) |
+         (var23 == 0 & var34 == 1 & var22 == 0) |
+         (var23 == 1 & var34 == 0 & var22 == 0) |
+         (var23 == 1 & var34 == 1 & var22 == 1) | 0);
+  assume((var24 == 0 & var33 == 0 & var23 == 1) |
+         (var24 == 0 & var33 == 1 & var23 == 0) |
+         (var24 == 1 & var33 == 0 & var23 == 0) |
+         (var24 == 1 & var33 == 1 & var23 == 1) | 0);
+  assume((var25 == 0 & var32 == 0 & var24 == 1) |
+         (var25 == 0 & var32 == 1 & var24 == 0) |
+         (var25 == 1 & var32 == 0 & var24 == 0) |
+         (var25 == 1 & var32 == 1 & var24 == 1) | 0);
+  assume((var26 == 0 & var31 == 0 & var25 == 1) |
+         (var26 == 0 & var31 == 1 & var25 == 0) |
+         (var26 == 1 & var31 == 0 & var25 == 0) |
+         (var26 == 1 & var31 == 1 & var25 == 1) | 0);
+  assume((var27 == 0 & var30 == 0 & var26 == 1) |
+         (var27 == 0 & var30 == 1 & var26 == 0) |
+         (var27 == 1 & var30 == 0 & var26 == 0) |
+         (var27 == 1 & var30 == 1 & var26 == 1) | 0);
+  assume((var15 == 0 & var42 == 0 & var14 == 1) |
+         (var15 == 0 & var42 == 1 & var14 == 0) |
+         (var15 == 1 & var42 == 0 & var14 == 0) |
+         (var15 == 1 & var42 == 1 & var14 == 1) | 0);
+  assume((var28 == 0 & var29 == 0 & var27 == 0) |
+         (var28 == 0 & var29 == 1 & var27 == 1) |
+         (var28 == 1 & var29 == 0 & var27 == 1) |
+         (var28 == 1 & var29 == 1 & var27 == 0) | 0);
+  reach_error();
+  return 0; /* 0 x[0]1 x[1]2 x[2]3 x[3]4 x[4]5 x[5]6 x[6]7 x[7]8 x[8]9 x[9]10
+               x[10]11 x[11]12 x[12]13 x[13]14 x[14]15 x[15]16 x[16]17 x[17]18
+               x[18]19 x[19]20 x[20]21 x[21]22 x[22]23 x[23]24 x[24]25 x[25]26
+               x[26]27 x[27]28 x[28]29 x[29]30 x[30]31 x[31]32 x[32]33 x[33]34
+               x[34]35 x[35]36 x[36]37 x[37]38 x[38]39 x[39]40 x[40]41 x[41]42
+               x[42]43 x[43]44 x[44] */
+}
+
+// CHECK: generated tests = 2
\ No newline at end of file