Correcting a mistake, universal variable was used in non-quantified formula

romainbrenguier · romainbrenguier · commit 3e9668a71e5e · 2017-06-06T10:35:50.000+01:00
diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -177,7 +177,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
     }
 
     or_exprt premise(
-      not_exprt(contains), binary_relation_exprt(qvar, ID_lt, offset));
+      not_exprt(contains), binary_relation_exprt(qvar2, ID_lt, offset));
     minus_exprt length_diff(haystack.length(), needle.length());
     string_constraintt a6(
       qvar2,

Original file line number	Diff line number	Diff line change
`@@ -177,7 +177,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(`
`177`	`177`	`}`
`178`	`178`
`179`	`179`	`or_exprt premise(`
`180`		`- not_exprt(contains), binary_relation_exprt(qvar, ID_lt, offset));`
	`180`	`+ not_exprt(contains), binary_relation_exprt(qvar2, ID_lt, offset));`
`181`	`181`	`minus_exprt length_diff(haystack.length(), needle.length());`
`182`	`182`	`string_constraintt a6(`
`183`	`183`	`qvar2,`