Merge pull request #3705 from tautschnig/fix-precondition

martin-cs · web-flow · commit 1f28ddd146ab · 2019-01-08T13:48:46.000Z
Fix precondition of string_insertion_builtin_functiont::eval
diff --git a/src/solvers/refinement/string_builtin_function.cpp b/src/solvers/refinement/string_builtin_function.cpp
@@ -445,7 +445,7 @@ std::vector<mp_integer> string_insertion_builtin_functiont::eval(
   const std::vector<mp_integer> &input2_value,
   const std::vector<mp_integer> &args_value) const
 {
-  PRECONDITION(args_value.size() >= 1 || args_value.size() <= 3);
+  PRECONDITION(args_value.size() >= 1 && args_value.size() <= 3);
   const auto offset = std::min(
     std::max(args_value[0], mp_integer(0)), mp_integer(input1_value.size()));
   const auto start = args_value.size() > 1

Original file line number	Diff line number	Diff line change
`@@ -445,7 +445,7 @@ std::vector<mp_integer> string_insertion_builtin_functiont::eval(`
`445`	`445`	`const std::vector<mp_integer> &input2_value,`
`446`	`446`	`const std::vector<mp_integer> &args_value) const`
`447`	`447`	`{`
`448`		`- PRECONDITION(args_value.size() >= 1 \|\| args_value.size() <= 3);`
	`448`	`+ PRECONDITION(args_value.size() >= 1 && args_value.size() <= 3);`
`449`	`449`	`const auto offset = std::min(`
`450`	`450`	`std::max(args_value[0], mp_integer(0)), mp_integer(input1_value.size()));`
`451`	`451`	`const auto start = args_value.size() > 1`