Handling of if_exprt in char array assignment

romainbrenguier · romainbrenguier · commit 30306f1fed9a · 2017-07-10T20:24:11.000+01:00
We handle that by calling constraint generation for "if" expressions.
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
@@ -218,12 +218,17 @@ bool string_refinementt::add_axioms_for_string_assigns(
       add_symbol_to_symbol_map(lhs, rhs);
       return false;
     }
-    else if(rhs.id() == ID_nondet_symbol)
+    else if(rhs.id()==ID_nondet_symbol)
     {
       add_symbol_to_symbol_map(
         lhs, generator.fresh_symbol("nondet_array", lhs.type()));
       return false;
     }
+    else if(rhs.id()==ID_if)
+    {
+      generator.add_axioms_for_if_array(lhs, to_if_expr(rhs));
+      return false;
+    }
     else
     {
       debug() << "string_refinement warning: not handling char_array: "

Original file line number	Diff line number	Diff line change
`@@ -218,12 +218,17 @@ bool string_refinementt::add_axioms_for_string_assigns(`
`218`	`218`	`add_symbol_to_symbol_map(lhs, rhs);`
`219`	`219`	`return false;`
`220`	`220`	`}`
`221`		`- else if(rhs.id() == ID_nondet_symbol)`
	`221`	`+ else if(rhs.id()==ID_nondet_symbol)`
`222`	`222`	`{`
`223`	`223`	`add_symbol_to_symbol_map(`
`224`	`224`	`lhs, generator.fresh_symbol("nondet_array", lhs.type()));`
`225`	`225`	`return false;`
`226`	`226`	`}`
	`227`	`+ else if(rhs.id()==ID_if)`
	`228`	`+ {`
	`229`	`+ generator.add_axioms_for_if_array(lhs, to_if_expr(rhs));`
	`230`	`+ return false;`
	`231`	`+ }`
`227`	`232`	`else`
`228`	`233`	`{`
`229`	`234`	`debug() << "string_refinement warning: not handling char_array: "`