Merge pull request #8180 from diffblue/smt2-extractbit

kroening · web-flow · commit 12660ce76ae8 · 2024-02-05T09:46:48.000-08:00
SMT2: fix extractbit with non-const index
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -1816,9 +1816,10 @@ void smt2_convt::convert_expr(const exprt &expr)
       // the arguments of the shift need to have the same width
       out << "(bvlshr ";
       flatten2bv(extractbit_expr.src());
+      out << ' ';
       typecast_exprt tmp(extractbit_expr.index(), extractbit_expr.src().type());
       convert_expr(tmp);
-      out << ")) bin1)"; // bvlshr, extract, =
+      out << ")) #b1)"; // bvlshr, extract, =
     }
   }
   else if(expr.id()==ID_extractbits)

Original file line number	Diff line number	Diff line change
`@@ -1816,9 +1816,10 @@ void smt2_convt::convert_expr(const exprt &expr)`
`1816`	`1816`	`// the arguments of the shift need to have the same width`
`1817`	`1817`	`out << "(bvlshr ";`
`1818`	`1818`	`flatten2bv(extractbit_expr.src());`
	`1819`	`+ out << ' ';`
`1819`	`1820`	`typecast_exprt tmp(extractbit_expr.index(), extractbit_expr.src().type());`
`1820`	`1821`	`convert_expr(tmp);`
`1821`		`- out << ")) bin1)"; // bvlshr, extract, =`
	`1822`	`+ out << ")) #b1)"; // bvlshr, extract, =`
`1822`	`1823`	`}`
`1823`	`1824`	`}`
`1824`	`1825`	`else if(expr.id()==ID_extractbits)`