Correcting misuse of univ variable qvar instead of qvar2

romainbrenguier · romainbrenguier · commit af98378f845a · 2017-06-06T12:34:52.000+01:00
diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -299,7 +299,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
     }
 
     or_exprt premise(
-      not_exprt(contains), binary_relation_exprt(qvar, ID_gt, offset));
+      not_exprt(contains), binary_relation_exprt(qvar2, ID_gt, offset));
     string_constraintt a6(
       qvar2,
       from_index,

Original file line number	Diff line number	Diff line change
`@@ -299,7 +299,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(`
`299`	`299`	`}`
`300`	`300`
`301`	`301`	`or_exprt premise(`
`302`		`- not_exprt(contains), binary_relation_exprt(qvar, ID_gt, offset));`
	`302`	`+ not_exprt(contains), binary_relation_exprt(qvar2, ID_gt, offset));`
`303`	`303`	`string_constraintt a6(`
`304`	`304`	`qvar2,`
`305`	`305`	`from_index,`