smt2 backend: fix constants

Daniel Kroening · Daniel Kroening · commit d37d2c62aa32 · 2018-11-24T16:31:08.000Z
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -2710,9 +2710,9 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
      expr_type.id()==ID_incomplete_c_enum ||
      expr_type.id()==ID_c_bit_field)
   {
-    const std::size_t width=boolbv_width(expr_type);
+    const std::size_t width = boolbv_width(expr_type);
 
-    const mp_integer value=bvrep2integer(expr.get_value(), width, false);
+    const mp_integer value = bvrep2integer(expr.get_value(), width, false);
 
     out << "(_ bv" << value
         << " " << width << ")";
@@ -2721,7 +2721,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
   {
     const fixedbv_spect spec(to_fixedbv_type(expr_type));
 
-    const mp_integer v=bvrep2integer(expr.get_value(), spec.width, false);
+    const mp_integer v = bvrep2integer(expr.get_value(), spec.width, false);
 
     out << "(_ bv" << v << " " << spec.width << ")";
   }

Original file line number	Diff line number	Diff line change
`@@ -2710,9 +2710,9 @@ void smt2_convt::convert_constant(const constant_exprt &expr)`
`2710`	`2710`	`expr_type.id()==ID_incomplete_c_enum \|\|`
`2711`	`2711`	`expr_type.id()==ID_c_bit_field)`
`2712`	`2712`	`{`
`2713`		`- const std::size_t width=boolbv_width(expr_type);`
	`2713`	`+ const std::size_t width = boolbv_width(expr_type);`
`2714`	`2714`
`2715`		`- const mp_integer value=bvrep2integer(expr.get_value(), width, false);`
	`2715`	`+ const mp_integer value = bvrep2integer(expr.get_value(), width, false);`
`2716`	`2716`
`2717`	`2717`	`out << "(_ bv" << value`
`2718`	`2718`	`<< " " << width << ")";`
`@@ -2721,7 +2721,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr)`
`2721`	`2721`	`{`
`2722`	`2722`	`const fixedbv_spect spec(to_fixedbv_type(expr_type));`
`2723`	`2723`
`2724`		`- const mp_integer v=bvrep2integer(expr.get_value(), spec.width, false);`
	`2724`	`+ const mp_integer v = bvrep2integer(expr.get_value(), spec.width, false);`
`2725`	`2725`
`2726`	`2726`	`out << "(_ bv" << v << " " << spec.width << ")";`
`2727`	`2727`	`}`