Use specific binary relation

Joel Allred · Joel Allred · commit 8cd17fefe611 · 2019-05-03T18:55:34.000+01:00
The specific version includes a typecheck.
diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp
@@ -740,8 +740,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   // All generated strings should have non-negative length
   for(const auto &string : generator.array_pool.created_strings())
   {
-    add_lemma(binary_relation_exprt{
-      string.length(), ID_ge, from_integer(0, string.length_type())});
+    add_lemma(greater_or_equal_to(
+      string.length(), from_integer(0, string.length_type())));
   }
 
   // Initial try without index set

Original file line number	Diff line number	Diff line change
`@@ -740,8 +740,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()`
`740`	`740`	`// All generated strings should have non-negative length`
`741`	`741`	`for(const auto &string : generator.array_pool.created_strings())`
`742`	`742`	`{`
`743`		`- add_lemma(binary_relation_exprt{`
`744`		`- string.length(), ID_ge, from_integer(0, string.length_type())});`
	`743`	`+ add_lemma(greater_or_equal_to(`
	`744`	`+ string.length(), from_integer(0, string.length_type())));`
`745`	`745`	`}`
`746`	`746`
`747`	`747`	`// Initial try without index set`