From 2a3760a6669f4a48e9c9944bf70f0cbbb45bd9b1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 29 Feb 2016 19:27:56 +0000 Subject: [PATCH] Use dstring constant for invalid pointer --- src/solvers/flattening/bv_pointers.cpp | 2 +- src/solvers/smt1/smt1_conv.cpp | 2 +- src/solvers/smt2/smt2_conv.cpp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 4567c89d7a4..78332162fdf 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -37,7 +37,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr) const exprt::operandst &operands=expr.operands(); - if(expr.id()=="invalid-pointer") + if(expr.id()==ID_invalid_pointer) { if(operands.size()==1 && is_ptr(operands[0].type())) diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp index a2e817ce724..6d8f3336f9f 100644 --- a/src/solvers/smt1/smt1_conv.cpp +++ b/src/solvers/smt1/smt1_conv.cpp @@ -1084,7 +1084,7 @@ void smt1_convt::convert_expr(const exprt &expr, bool bool_as_bv) { convert_is_dynamic_object(expr, bool_as_bv); } - else if(expr.id()=="invalid-pointer") + else if(expr.id()==ID_invalid_pointer) { const typet &type=expr.type(); diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index e0dff532113..41c0e933d67 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1573,7 +1573,7 @@ void smt2_convt::convert_expr(const exprt &expr) { convert_is_dynamic_object(expr); } - else if(expr.id()=="invalid-pointer") + else if(expr.id()==ID_invalid_pointer) { assert(expr.operands().size()==1);