Record all output for tests

cvc5.json

@@ -0,0 +1,6 @@
+{
+    "name": "cvc5",
+    "args": ["verify", "--solver-type=cvc5"],
+    "filter": "^(.*\\.c)$",
+    "timeout": 60
+}

src/example-archive/Rust/broken/error-cerberus/00002-memory-leaks.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+/home/dhruv/.opam/5.2.0/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
+int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
+    ^~~~~~~ 

src/example-archive/Rust/broken/error-cerberus/00002-memory-leaks.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+/home/dhruv/.opam/5.2.0/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
+int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
+    ^~~~~~~ 

src/example-archive/Rust/broken/error-cerberus/00003-string-transfer.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+/home/dhruv/.opam/5.2.0/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
+int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
+    ^~~~~~~ 

src/example-archive/Rust/broken/error-cerberus/00003-string-transfer.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+/home/dhruv/.opam/5.2.0/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
+int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
+    ^~~~~~~ 

src/example-archive/Rust/broken/error-cerberus/00005-lifetimes.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+/home/dhruv/.opam/5.2.0/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
+int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
+    ^~~~~~~ 

src/example-archive/Rust/broken/error-cerberus/00005-lifetimes.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+/home/dhruv/.opam/5.2.0/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
+int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
+    ^~~~~~~ 

src/example-archive/Rust/broken/error-proof/00001-memory-leaks-no-print.c.cvc5

@@ -0,0 +1,5 @@
+return code: 1
+[1/1]: main -- fail
+./src/example-archive/Rust/broken/error-proof/00001-memory-leaks-no-print.c:29:18: error: Unknown function 'malloc_proxy'
+  int *my_data = malloc(sizeof(int)); // Allocate memory for an integer on the heap
+                 ^~~~~~ 

src/example-archive/Rust/broken/error-proof/00001-memory-leaks-no-print.c.z3

@@ -0,0 +1,5 @@
+return code: 1
+[1/1]: main -- fail
+./src/example-archive/Rust/broken/error-proof/00001-memory-leaks-no-print.c:29:18: error: Unknown function 'malloc_proxy'
+  int *my_data = malloc(sizeof(int)); // Allocate memory for an integer on the heap
+                 ^~~~~~ 

src/example-archive/Rust/broken/error-proof/00004-simple-lifetimes.c.cvc5

@@ -0,0 +1,11 @@
+return code: 1
+./src/example-archive/Rust/broken/error-proof/00004-simple-lifetimes.c:35:15: warning: CN pointer equality is not the same as C's (will not warn again). Please use `ptr_eq` or `is_null` (maybe `addr_eq`).
+              return == input; 
+              ~~~~~~~^~~~~~~~ 
+[1/2]: borrow -- pass
+[2/2]: main -- fail
+./src/example-archive/Rust/broken/error-proof/00004-simple-lifetimes.c:44:15: error: Missing resource for reading
+    int ret = *r; // Safe to use 'r' here, as 'x' is still in scope
+              ^~ 
+Resource needed: Owned<signed int>(call_borrow0.return)
+State file: file:///tmp/state__00004-simple-lifetimes.c__main.html

src/example-archive/Rust/broken/error-proof/00004-simple-lifetimes.c.z3

@@ -0,0 +1,11 @@
+return code: 1
+./src/example-archive/Rust/broken/error-proof/00004-simple-lifetimes.c:35:15: warning: CN pointer equality is not the same as C's (will not warn again). Please use `ptr_eq` or `is_null` (maybe `addr_eq`).
+              return == input; 
+              ~~~~~~~^~~~~~~~ 
+[1/2]: borrow -- pass
+[2/2]: main -- fail
+./src/example-archive/Rust/broken/error-proof/00004-simple-lifetimes.c:44:15: error: Missing resource for reading
+    int ret = *r; // Safe to use 'r' here, as 'x' is still in scope
+              ^~ 
+Resource needed: Owned<signed int>(call_borrow0.return)
+State file: file:///tmp/state__00004-simple-lifetimes.c__main.html

src/example-archive/Rust/broken/error-proof/00006-lifetimes-broken.c.cvc5

@@ -0,0 +1,11 @@
+return code: 1
+./src/example-archive/Rust/broken/error-proof/00006-lifetimes-broken.c:37:15: warning: CN pointer equality is not the same as C's (will not warn again). Please use `ptr_eq` or `is_null` (maybe `addr_eq`).
+              return == input; 
+              ~~~~~~~^~~~~~~~ 
+[1/2]: borrow -- pass
+[2/2]: main -- fail
+./src/example-archive/Rust/broken/error-proof/00006-lifetimes-broken.c:51:2: error: Missing resource for writing
+	global_int = *r;
+	~~~~~~~~~~~^~~~ 
+Resource needed: Block<signed int>(&global_int)
+State file: file:///tmp/state__00006-lifetimes-broken.c__main.html

src/example-archive/Rust/broken/error-proof/00006-lifetimes-broken.c.z3

@@ -0,0 +1,11 @@
+return code: 1
+./src/example-archive/Rust/broken/error-proof/00006-lifetimes-broken.c:37:15: warning: CN pointer equality is not the same as C's (will not warn again). Please use `ptr_eq` or `is_null` (maybe `addr_eq`).
+              return == input; 
+              ~~~~~~~^~~~~~~~ 
+[1/2]: borrow -- pass
+[2/2]: main -- fail
+./src/example-archive/Rust/broken/error-proof/00006-lifetimes-broken.c:51:2: error: Missing resource for writing
+	global_int = *r;
+	~~~~~~~~~~~^~~~ 
+Resource needed: Block<signed int>(&global_int)
+State file: file:///tmp/state__00006-lifetimes-broken.c__main.html

src/example-archive/Rust/broken/error-proof/00007-string-transfer-no-io.c.cvc5

@@ -0,0 +1,14 @@
+return code: 1
+[1/3]: create_string -- fail
+[2/3]: copy_to_global -- fail
+[3/3]: main -- fail
+./src/example-archive/Rust/broken/error-proof/00007-string-transfer-no-io.c:41:15: error: Unknown function 'malloc_proxy'
+    char *s = malloc(20 * sizeof(char));  // Allocate memory for the string
+              ^~~~~~ 
+./src/example-archive/Rust/broken/error-proof/00007-string-transfer-no-io.c:51:31: error: Mismatched types.
+    strncpy(global_string, s, sizeof(global_string) - 1);
+                              ~~~~~~~~~~~~~~~~~~~~~~^~~ 
+Expected value of type 'u64' but found value of type 'u32'
+./src/example-archive/Rust/broken/error-proof/00007-string-transfer-no-io.c:62:5: error: Unknown function 'free_proxy'
+    free(my_string);  // Explicitly free the memory allocated in create_string
+    ^~~~ 

src/example-archive/Rust/broken/error-proof/00007-string-transfer-no-io.c.z3

@@ -0,0 +1,14 @@
+return code: 1
+[1/3]: create_string -- fail
+[2/3]: copy_to_global -- fail
+[3/3]: main -- fail
+./src/example-archive/Rust/broken/error-proof/00007-string-transfer-no-io.c:41:15: error: Unknown function 'malloc_proxy'
+    char *s = malloc(20 * sizeof(char));  // Allocate memory for the string
+              ^~~~~~ 
+./src/example-archive/Rust/broken/error-proof/00007-string-transfer-no-io.c:51:31: error: Mismatched types.
+    strncpy(global_string, s, sizeof(global_string) - 1);
+                              ~~~~~~~~~~~~~~~~~~~~~~^~~ 
+Expected value of type 'u64' but found value of type 'u32'
+./src/example-archive/Rust/broken/error-proof/00007-string-transfer-no-io.c:62:5: error: Unknown function 'free_proxy'
+    free(my_string);  // Explicitly free the memory allocated in create_string
+    ^~~~ 

src/example-archive/SAW/broken/error-cerberus/00001.swap.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+/home/dhruv/.opam/5.2.0/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
+int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
+    ^~~~~~~ 

src/example-archive/SAW/broken/error-cerberus/00001.swap.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+/home/dhruv/.opam/5.2.0/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
+int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
+    ^~~~~~~ 

src/example-archive/SAW/broken/error-cerberus/00007.u128.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/SAW/broken/error-cerberus/00007.u128.c:83:13: error: use of undeclared identifier 'bcmp'
+    return !bcmp(x, y, 16);
+            ^

src/example-archive/SAW/broken/error-cerberus/00007.u128.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/SAW/broken/error-cerberus/00007.u128.c:83:13: error: use of undeclared identifier 'bcmp'
+    return !bcmp(x, y, 16);
+            ^

src/example-archive/SAW/broken/error-cerberus/00008.salsa20.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/SAW/broken/error-cerberus/salsa20.h:67:37: error: feature not yet supported: array parameter with the static keyword
+                            uint8_t nonce[static 8],
+                                    ^~~~~~~~~~~~~~~ 

src/example-archive/SAW/broken/error-cerberus/00008.salsa20.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/SAW/broken/error-cerberus/salsa20.h:67:37: error: feature not yet supported: array parameter with the static keyword
+                            uint8_t nonce[static 8],
+                                    ^~~~~~~~~~~~~~~ 

src/example-archive/SAW/broken/error-proof/00002.popcount.c.cvc5

@@ -0,0 +1,9 @@
+return code: 1
+[1/3]: pop_count -- pass
+[2/3]: pop_count_mul -- pass
+[3/3]: pop_count_sparse -- fail
+./src/example-archive/SAW/broken/error-proof/00002.popcount.c:66:13: error: Undefined behaviour
+        n = n + 1;
+            ~~^~~ 
+an exceptional condition occurs during the evaluation of an expression (§6.5#5)
+State file: file:///tmp/state__00002.popcount.c__pop_count_sparse.html

src/example-archive/SAW/broken/error-proof/00002.popcount.c.z3

@@ -0,0 +1,9 @@
+return code: 1
+[1/3]: pop_count -- pass
+[2/3]: pop_count_mul -- pass
+[3/3]: pop_count_sparse -- fail
+./src/example-archive/SAW/broken/error-proof/00002.popcount.c:66:13: error: Undefined behaviour
+        n = n + 1;
+            ~~^~~ 
+an exceptional condition occurs during the evaluation of an expression (§6.5#5)
+State file: file:///tmp/state__00002.popcount.c__pop_count_sparse.html

src/example-archive/SAW/broken/error-proof/00003.point.c.cvc5

@@ -0,0 +1 @@
+TIMEOUT

src/example-archive/SAW/broken/error-proof/00003.point.c.z3

@@ -0,0 +1,15 @@
+return code: 1
+[1/4]: point_eq -- fail
+[2/4]: point_new -- fail
+[3/4]: point_copy -- pass
+[4/4]: point_add -- pass
+./src/example-archive/SAW/broken/error-proof/00003.point.c:116:5: error: Unprovable constraint
+    return p1->x == p2->x && p1->y == p2-> y;
+    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+Constraint from ./src/example-archive/SAW/broken/error-proof/00003.point.c:109:7:
+	     if (vp11.x == vp21.x && vp11.y == vp21.x) {
+	     ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+State file: file:///tmp/state__00003.point.c__point_eq.html
+./src/example-archive/SAW/broken/error-proof/00003.point.c:131:18: error: Unknown function 'malloc_proxy'
+    point* ret = malloc(sizeof(point));
+                 ^~~~~~ 

src/example-archive/SAW/broken/error-proof/00004.tutorial-dotprod.c.cvc5

@@ -0,0 +1,5 @@
+return code: 1
+./src/example-archive/SAW/broken/error-proof/00004.tutorial-dotprod.c:53:5: error: unexpected token after '}' and before 'ensures'
+parsing "condition": seen "CN_TAKE LNAME VARIABLE EQ resource", expecting "SEMICOLON"
+    ensures  take ax1 = each(u32 j; 0u32 <= j && j < size) { Owned<uint32_t>(array_shift<uint32_t>(x,j)) };
+    ^~~~~~~ 

src/example-archive/SAW/broken/error-proof/00004.tutorial-dotprod.c.z3

@@ -0,0 +1,5 @@
+return code: 1
+./src/example-archive/SAW/broken/error-proof/00004.tutorial-dotprod.c:53:5: error: unexpected token after '}' and before 'ensures'
+parsing "condition": seen "CN_TAKE LNAME VARIABLE EQ resource", expecting "SEMICOLON"
+    ensures  take ax1 = each(u32 j; 0u32 <= j && j < size) { Owned<uint32_t>(array_shift<uint32_t>(x,j)) };
+    ^~~~~~~ 

src/example-archive/SAW/broken/error-proof/00006.tutorial-ffs.c.cvc5

@@ -0,0 +1,27 @@
+return code: 1
+[1/5]: ffs_ref -- fail
+[2/5]: ffs_imp -- pass
+[3/5]: ffs_imp_nobranch -- pass
+[4/5]: ffs_bug -- pass
+[5/5]: ffs_musl -- fail
+./src/example-archive/SAW/broken/error-proof/00006.tutorial-ffs.c:42:19: error: Undefined behaviour
+        if(((1 << i++) & word) != 0)
+                  ~^~ 
+an exceptional condition occurs during the evaluation of an expression (§6.5#5)
+State file: file:///tmp/state__00006.tutorial-ffs.c__ffs_ref.html
+./src/example-archive/SAW/broken/error-proof/00006.tutorial-ffs.c:103:14: error: Missing resource for reading
+  return x ? debruijn32[(x&-x)*0x076be629 >> 27]+1 : 0;
+             ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+Resource needed: Owned<char>(&(&&debruijn32[(u64)0'i32])[(u64)(
+                                                           !(
+                                                             0'i32
+                                                             <= 27'i32 /* 0x1b */
+                                                             && true
+                                                           ) ? 0'u32 :
+                                                           (
+                                                             (x & 0'u32 - x)
+                                                             * (u32)124511785'i32 /* 0x76be629 */
+                                                             >> (u32)27'i32 /* 0x1b */
+                                                           )
+                                                         )])
+State file: file:///tmp/state__00006.tutorial-ffs.c__ffs_musl.html

src/example-archive/SAW/broken/error-proof/00006.tutorial-ffs.c.z3

@@ -0,0 +1,27 @@
+return code: 1
+[1/5]: ffs_ref -- fail
+[2/5]: ffs_imp -- pass
+[3/5]: ffs_imp_nobranch -- pass
+[4/5]: ffs_bug -- pass
+[5/5]: ffs_musl -- fail
+./src/example-archive/SAW/broken/error-proof/00006.tutorial-ffs.c:42:19: error: Undefined behaviour
+        if(((1 << i++) & word) != 0)
+                  ~^~ 
+an exceptional condition occurs during the evaluation of an expression (§6.5#5)
+State file: file:///tmp/state__00006.tutorial-ffs.c__ffs_ref.html
+./src/example-archive/SAW/broken/error-proof/00006.tutorial-ffs.c:103:14: error: Missing resource for reading
+  return x ? debruijn32[(x&-x)*0x076be629 >> 27]+1 : 0;
+             ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+Resource needed: Owned<char>(&(&&debruijn32[(u64)0'i32])[(u64)(
+                                                           !(
+                                                             0'i32
+                                                             <= 27'i32 /* 0x1b */
+                                                             && true
+                                                           ) ? 0'u32 :
+                                                           (
+                                                             (x & 0'u32 - x)
+                                                             * (u32)124511785'i32 /* 0x76be629 */
+                                                             >> (u32)27'i32 /* 0x1b */
+                                                           )
+                                                         )])
+State file: file:///tmp/state__00006.tutorial-ffs.c__ffs_musl.html

src/example-archive/SAW/working/00005.tutorial-double.c.cvc5

@@ -0,0 +1,3 @@
+return code: 0
+[1/2]: double_ref -- pass
+[2/2]: double_imp -- pass

src/example-archive/SAW/working/00005.tutorial-double.c.z3

@@ -0,0 +1,3 @@
+return code: 0
+[1/2]: double_ref -- pass
+[2/2]: double_imp -- pass

src/example-archive/c-testsuite/broken/error-cerberus/00025.err2.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00025.err2.c:15:9: error: use of undeclared identifier 'strlen'
+	return strlen(p) - 5;
+        ^

src/example-archive/c-testsuite/broken/error-cerberus/00025.err2.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00025.err2.c:15:9: error: use of undeclared identifier 'strlen'
+	return strlen(p) - 5;
+        ^

src/example-archive/c-testsuite/broken/error-cerberus/00042.err2.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00042.err2.c:4:2: error: unsupported union types
+	union { int a; int b; } u;
+	^~~~~~~~~~~~~~~~~~~~~~~ 

src/example-archive/c-testsuite/broken/error-cerberus/00042.err2.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00042.err2.c:4:2: error: unsupported union types
+	union { int a; int b; } u;
+	^~~~~~~~~~~~~~~~~~~~~~~ 

src/example-archive/c-testsuite/broken/error-cerberus/00046.err2.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00046.err2.c:3:2: error: unsupported union types
+	union {
+	^~~~~~~ 

src/example-archive/c-testsuite/broken/error-cerberus/00046.err2.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00046.err2.c:3:2: error: unsupported union types
+	union {
+	^~~~~~~ 

src/example-archive/c-testsuite/broken/error-cerberus/00050.err2.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00050.err2.c:21:25: error: undefined behaviour: the initializer for a scalar shall be a single expression
+struct S2 v = {1, 2, 3, {4, 5}};
+                        ^~~~~~ 

src/example-archive/c-testsuite/broken/error-cerberus/00050.err2.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00050.err2.c:21:25: error: undefined behaviour: the initializer for a scalar shall be a single expression
+struct S2 v = {1, 2, 3, {4, 5}};
+                        ^~~~~~ 

src/example-archive/c-testsuite/broken/error-cerberus/00056.err2.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+/home/dhruv/.opam/5.2.0/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
+int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
+    ^~~~~~~ 

src/example-archive/c-testsuite/broken/error-cerberus/00056.err2.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+/home/dhruv/.opam/5.2.0/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
+int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
+    ^~~~~~~ 

src/example-archive/c-testsuite/broken/error-cerberus/00087.err2.c.cvc5

@@ -0,0 +1,3 @@
+return code: 2
+unknown location  error: CoreTyping_TODO(the first operand of ccall() should have a C function type)
+error: this is likely a bug in the Core elaboration.

src/example-archive/c-testsuite/broken/error-cerberus/00087.err2.c.z3

@@ -0,0 +1,3 @@
+return code: 2
+unknown location  error: CoreTyping_TODO(the first operand of ccall() should have a C function type)
+error: this is likely a bug in the Core elaboration.

src/example-archive/c-testsuite/broken/error-cerberus/00089.err2.c.cvc5

@@ -0,0 +1,3 @@
+return code: 2
+unknown location  error: CoreTyping_TODO(the first operand of ccall() should have a C function type)
+error: this is likely a bug in the Core elaboration.

src/example-archive/c-testsuite/broken/error-cerberus/00089.err2.c.z3

@@ -0,0 +1,3 @@
+return code: 2
+unknown location  error: CoreTyping_TODO(the first operand of ccall() should have a C function type)
+error: this is likely a bug in the Core elaboration.

src/example-archive/c-testsuite/broken/error-cerberus/00095.err2.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00095.err2.c:10:9: error: constraint violation: incompatible pointer types returning 'signed int (*) (void)' from a function with result type 'void*'
+	return &main;
+	^      ~~~~~ 

src/example-archive/c-testsuite/broken/error-cerberus/00095.err2.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00095.err2.c:10:9: error: constraint violation: incompatible pointer types returning 'signed int (*) (void)' from a function with result type 'void*'
+	return &main;
+	^      ~~~~~ 

src/example-archive/c-testsuite/broken/error-cerberus/00113.err2.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00113.err2.c:3:1: error: Unsupported C-type float
+{
+~      ^

src/example-archive/c-testsuite/broken/error-cerberus/00113.err2.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00113.err2.c:3:1: error: Unsupported C-type float
+{
+~      ^

src/example-archive/c-testsuite/broken/error-cerberus/00119.err2.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00119.err2.c:1:8: error: Unsupported C-type double
+double x = 100;
+       ^ 

src/example-archive/c-testsuite/broken/error-cerberus/00119.err2.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00119.err2.c:1:8: error: Unsupported C-type double
+double x = 100;
+       ^ 

src/example-archive/c-testsuite/broken/error-cerberus/00123.err2.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00123.err2.c:1:8: error: Unsupported C-type double
+double x = 100.0;
+       ^ 

src/example-archive/c-testsuite/broken/error-cerberus/00123.err2.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+./src/example-archive/c-testsuite/broken/error-cerberus/00123.err2.c:1:8: error: Unsupported C-type double
+double x = 100.0;
+       ^ 

src/example-archive/c-testsuite/broken/error-cerberus/00125.err2.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+/home/dhruv/.opam/5.2.0/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
+int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
+    ^~~~~~~ 

src/example-archive/c-testsuite/broken/error-cerberus/00125.err2.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+/home/dhruv/.opam/5.2.0/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
+int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
+    ^~~~~~~ 

src/example-archive/c-testsuite/broken/error-cerberus/00131.err2.c.cvc5

@@ -0,0 +1,4 @@
+return code: 2
+/home/dhruv/.opam/5.2.0/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
+int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
+    ^~~~~~~ 

src/example-archive/c-testsuite/broken/error-cerberus/00131.err2.c.z3

@@ -0,0 +1,4 @@
+return code: 2
+/home/dhruv/.opam/5.2.0/lib/cerberus/runtime/libc/include/stdio.h:58:5: error: unsupported variadic functions
+int fprintf(FILE * restrict stream, const char * restrict fmt, ...);
+    ^~~~~~~