Simplify dec_solve

romainbrenguier · romainbrenguier · commit 13e87a9a4caf · 2018-04-23T08:50:11.000+01:00
Result is not modified, and the last return is never reached.
diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp
@@ -477,16 +477,12 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()
 
   statistics() << "Solving with " << prop.solver_text() << eom;
 
-  propt::resultt result=prop.prop_solve();
-
-  switch(result)
+  switch(prop.prop_solve())
   {
     case propt::resultt::P_SATISFIABLE: return resultt::D_SATISFIABLE;
     case propt::resultt::P_UNSATISFIABLE: return resultt::D_UNSATISFIABLE;
     default: return resultt::D_ERROR;
   }
-
-  return resultt::D_ERROR;
 }
 
 exprt prop_conv_solvert::get(const exprt &expr) const

Original file line number	Diff line number	Diff line change
`@@ -477,16 +477,12 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()`
`477`	`477`
`478`	`478`	`statistics() << "Solving with " << prop.solver_text() << eom;`
`479`	`479`
`480`		`- propt::resultt result=prop.prop_solve();`
`481`		`-`
`482`		`- switch(result)`
	`480`	`+ switch(prop.prop_solve())`
`483`	`481`	`{`
`484`	`482`	`case propt::resultt::P_SATISFIABLE: return resultt::D_SATISFIABLE;`
`485`	`483`	`case propt::resultt::P_UNSATISFIABLE: return resultt::D_UNSATISFIABLE;`
`486`	`484`	`default: return resultt::D_ERROR;`
`487`	`485`	`}`
`488`		`-`
`489`		`- return resultt::D_ERROR;`
`490`	`486`	`}`
`491`	`487`
`492`	`488`	`exprt prop_conv_solvert::get(const exprt &expr) const`