From 112d11168ce947e91d4568d068fc4030a83869d3 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 21 Nov 2023 11:51:06 +0000 Subject: [PATCH] Run additional regressions with new SMT solver Adding other 2 regression tests now passing to be run with new SMT solver Specifically: - dynamic_size1/stack_object.desc - ptr_arithmetic_on_null/type_conflict.desc --- regression/cbmc/dynamic_size1/stack_object.desc | 2 +- regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/cbmc/dynamic_size1/stack_object.desc b/regression/cbmc/dynamic_size1/stack_object.desc index c6ac74c15fb..242e2c1d4c0 100644 --- a/regression/cbmc/dynamic_size1/stack_object.desc +++ b/regression/cbmc/dynamic_size1/stack_object.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE stack_object.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc b/regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc index c7a44b02a42..0f5cbf5fcea 100644 --- a/regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc +++ b/regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc @@ -1,4 +1,4 @@ -CORE gcc-only no-new-smt +CORE gcc-only main.c -DMISSING_CAST pointer subtraction over different types