diff --git a/include/klee-test-comp.c b/include/klee-test-comp.c
index ecda66ba02..bad3b783d0 100644
--- a/include/klee-test-comp.c
+++ b/include/klee-test-comp.c
@@ -33,6 +33,12 @@ unsigned int __VERIFIER_nondet_uint(void) {
   return x;
 }
 
+unsigned __int128 __VERIFIER_nondet_uint128(void) {
+  unsigned __int128 x;
+  klee_make_symbolic(&x, sizeof(x), "unsigned __int128");
+  return x;
+}
+
 unsigned __VERIFIER_nondet_unsigned(void) {
   unsigned x;
   klee_make_symbolic(&x, sizeof(x), "unsigned");
diff --git a/test/Feature/uint128.c b/test/Feature/uint128.c
new file mode 100644
index 0000000000..efa5915beb
--- /dev/null
+++ b/test/Feature/uint128.c
@@ -0,0 +1,11 @@
+// RUN: %clang %s -emit-llvm %O0opt -c -g -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s
+// CHECK-NOT: failed external call
+#include "klee-test-comp.c"
+extern unsigned __int128 __VERIFIER_nondet_uint128();
+
+int main() {
+  __int128 x = __VERIFIER_nondet_uint128();
+  return x > 0;
+}