Fixed function inversion.

jasigal · jasigal · commit a1c44e1031f9 · 2017-06-29T17:04:20.000+01:00
Now takes into account the multi-arity of plus (was previously assumed to be binary).
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
@@ -1076,8 +1076,10 @@ std::map<exprt, int> string_refinementt::map_representation_of_sum(
     to_process.pop_back();
     if(cur.id()==ID_plus)
     {
-      to_process.push_back(std::make_pair(cur.op1(), positive));
-      to_process.push_back(std::make_pair(cur.op0(), positive));
+      for(const exprt &op : cur.operands())
+      {
+        to_process.push_back(std::make_pair(op, positive));
+      }
     }
     else if(cur.id()==ID_minus)
     {

Original file line number	Diff line number	Diff line change
`@@ -1076,8 +1076,10 @@ std::map<exprt, int> string_refinementt::map_representation_of_sum(`
`1076`	`1076`	`to_process.pop_back();`
`1077`	`1077`	`if(cur.id()==ID_plus)`
`1078`	`1078`	`{`
`1079`		`- to_process.push_back(std::make_pair(cur.op1(), positive));`
`1080`		`- to_process.push_back(std::make_pair(cur.op0(), positive));`
	`1079`	`+ for(const exprt &op : cur.operands())`
	`1080`	`+ {`
	`1081`	`+ to_process.push_back(std::make_pair(op, positive));`
	`1082`	`+ }`
`1081`	`1083`	`}`
`1082`	`1084`	`else if(cur.id()==ID_minus)`
`1083`	`1085`	`{`