From eae5bca4498bcc9e22ed80c3480d043b3e6f72d6 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 31 Dec 2018 18:44:08 +0000 Subject: [PATCH 1/2] smt2: add a missing space --- src/solvers/smt2/smt2_conv.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 2ab17ef6c77..b14ef75230e 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -3611,7 +3611,7 @@ void smt2_convt::convert_with(const with_exprt &expr) // the member is at the end out << "(concat "; convert_expr(value); - out << "((_ extract " << (m.offset-1) << " 0) ?withop))"; + out << " ((_ extract " << (m.offset - 1) << " 0) ?withop))"; } else { From aae639ab6bdd5341bac78711d074104e2c5f680e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 31 Dec 2018 19:25:23 +0000 Subject: [PATCH 2/2] smt2 frontend: let identifiers must be globally unique The solver backend assumes that identifiers used in let expressions are globally unique. The renamed identifiers are now retained in the id_map to ensure that they are not re-used. This enables 11 regression tests to pass. --- scripts/delete_failing_smt2_solver_tests | 11 ----------- src/solvers/smt2/smt2_parser.cpp | 5 ++--- 2 files changed, 2 insertions(+), 14 deletions(-) diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests index 36c45a78d25..cba0a131902 100755 --- a/scripts/delete_failing_smt2_solver_tests +++ b/scripts/delete_failing_smt2_solver_tests @@ -7,7 +7,6 @@ rm Bitfields3/test.desc rm Empty_struct1/test.desc rm Endianness4/test.desc rm Endianness6/test.desc -rm Endianness7/test.desc rm Float-div2/test.desc rm Float-div3/test.desc rm Float-no-simp1/test.desc @@ -37,25 +36,19 @@ rm Linking4/test.desc rm Linking7/test.desc rm Linking7/member-name-mismatch.desc rm Malloc23/test.desc -rm Malloc24/test.desc -rm Memory_leak2/test.desc rm Multi_Dimensional_Array2/test.desc rm Overflow_Leftshift1/test.desc rm Overflow_Subtraction1/test.desc rm Pointer_Arithmetic11/test.desc rm Pointer_byte_extract2/test.desc -rm Pointer_byte_extract3/test.desc -rm Pointer_byte_extract4/test.desc rm Pointer_byte_extract5/no-simplify.desc rm Pointer_byte_extract5/test.desc -rm Pointer_byte_extract7/test.desc rm Pointer_byte_extract9/test.desc rm Promotion3/test.desc rm Quantifiers-assertion/test.desc rm Quantifiers-assignment/test.desc rm Quantifiers-invalid-var-range/test.desc rm Quantifiers-type/test.desc -rm Struct_Bytewise2/test.desc rm Union_Initialization1/test.desc rm address_space_size_limit1/test.desc rm array-function-parameters/test.desc @@ -71,20 +64,16 @@ rm byte_update8/test.desc rm byte_update9/test.desc rm compact-trace/test.desc rm dynamic_size1/stack_object.desc -rm equality_through_struct_containing_arrays1/test.desc -rm equality_through_struct_containing_arrays2/test.desc rm graphml_witness1/test.desc rm integer-assignments1/test.desc rm memory_allocation1/test.desc rm pointer-function-parameters-struct-mutual-recursion/test.desc rm pointer-function-parameters-struct-simple-recursion/test.desc rm pointer-function-parameters-struct-simple-recursion-2/test.desc -rm pointer-function-parameters-struct-simple-recursion-3/test.desc rm scanf1/test.desc rm stack-trace/test.desc rm struct6/test.desc rm struct7/test.desc -rm struct9/test.desc rm trace-values/trace-values.desc rm trace_show_function_calls/test.desc rm union12/test.desc diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index 0f53371a14e..860bda52064 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -206,9 +206,8 @@ exprt smt2_parsert::let_expression() result=let; } - // remove bindings from id_map - for(const auto &b : bindings) - id_map.erase(b.first); + // we keep these in the id_map in order to retain globally + // unique identifiers // restore renamings renaming_map=old_renaming_map;