From c06ade8ef96b87fc0c94456b7bd386f4e4e8b095 Mon Sep 17 00:00:00 2001
From: Yurii Kostyukov <kostyukov.yurii@gmail.com>
Date: Mon, 23 Oct 2023 14:14:33 +0300
Subject: [PATCH 1/2] [fix] Propagation of without filter

---
 lib/Core/TargetManager.h              |  6 +-
 test/Industry/egcd3-ll_valuebound10.c | 85 +++++++++++++++++++++++++++
 2 files changed, 90 insertions(+), 1 deletion(-)
 create mode 100644 test/Industry/egcd3-ll_valuebound10.c

diff --git a/lib/Core/TargetManager.h b/lib/Core/TargetManager.h
index c135f354dd..ba2dea9ab3 100644
--- a/lib/Core/TargetManager.h
+++ b/lib/Core/TargetManager.h
@@ -136,7 +136,11 @@ class TargetHistoryTargetPairToStatesMap final {
   inline map_it begin() noexcept { return self.begin(); }
   inline map_it end() noexcept { return self.end(); }
 
-  inline const cv at(const k &__k) const { return self.at(__k); }
+  inline const cv at(const k &__k) const {
+    cv result = self.at(__k);
+    result.setWithout(without);
+    return result;
+  }
   inline it begin() const noexcept { return it(self.begin(), without); };
   inline it end() const noexcept { return it(self.end(), without); };
 
diff --git a/test/Industry/egcd3-ll_valuebound10.c b/test/Industry/egcd3-ll_valuebound10.c
new file mode 100644
index 0000000000..5fd1bc76d1
--- /dev/null
+++ b/test/Industry/egcd3-ll_valuebound10.c
@@ -0,0 +1,85 @@
+// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state %t1.bc
+// RUN: %klee-stats --print-columns 'BCov(%)' --table-format=csv %t.klee-out > %t.stats
+// RUN: FileCheck -input-file=%t.stats %s
+// CHECK: BCov(%)
+// CHECK-NEXT: {{(8[5-9]|9[0-9]|100)\.}}
+
+#include "klee-test-comp.c"
+/* extended Euclid's algorithm */
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "egcd3-ll.c", 4, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    int x, y;
+    long long a, b, p, q, r, s;
+    x = __VERIFIER_nondet_int();
+    assume_abort_if_not(x>=0 && x<=10);
+    y = __VERIFIER_nondet_int();
+    assume_abort_if_not(y>=0 && y<=10);
+    assume_abort_if_not(x >= 1);
+    assume_abort_if_not(y >= 1);
+
+    a = x;
+    b = y;
+    p = 1;
+    q = 0;
+    r = 0;
+    s = 1;
+
+    while (1) {
+        if (!(b != 0))
+            break;
+        long long c, k;
+        c = a;
+        k = 0;
+
+        while (1) {
+            if (!(c >= b))
+                break;
+            long long d, v;
+            d = 1;
+            v = b;
+
+            while (1) {
+                __VERIFIER_assert(a == y * r + x * p);
+                __VERIFIER_assert(b == x * q + y * s);
+                __VERIFIER_assert(a == k * b + c);
+                __VERIFIER_assert(v == b * d);
+
+                if (!(c >= 2 * v))
+                    break;
+                d = 2 * d;
+                v = 2 * v;
+            }
+            c = c - v;
+            k = k + d;
+        }
+
+        a = b;
+        b = c;
+        long long temp;
+        temp = p;
+        p = q;
+        q = temp - q * k;
+        temp = r;
+        r = s;
+        s = temp - s * k;
+    }
+    __VERIFIER_assert(p*x - q*x + r*y - s*y  == a);
+    return 0;
+}

From 5c9950e3dc462b6df5308c64e6b1d5ce1c3679ff Mon Sep 17 00:00:00 2001
From: Yurii Kostyukov <kostyukov.yurii@gmail.com>
Date: Mon, 23 Oct 2023 17:57:17 +0300
Subject: [PATCH 2/2] [fix] Small fixes

---
 lib/Core/Executor.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index dd34b18d5d..25a7254115 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -6021,13 +6021,13 @@ void Executor::executeMemoryOperation(
     bool success = solver->getResponse(state->constraints.cs(), inBounds,
                                        response, state->queryMetaData);
     solver->setTimeout(time::Span());
-    bool mustBeInBounds = !isa<InvalidResponse>(response);
     if (!success) {
       state->pc = state->prevPC;
       terminateStateOnSolverError(*state, "Query timed out (bounds check).");
       return;
     }
 
+    bool mustBeInBounds = !isa<InvalidResponse>(response);
     if (mustBeInBounds) {
       if (isa<UnknownResponse>(response)) {
         addConstraint(*state, inBounds);