oe

Author: chriseth

src/encoder.rs

@@ -154,7 +154,7 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
     pub fn encode_function(
         &mut self,
         function: &FunctionDefinition,
-        arguments: &Vec<SMTVariable>,
+        arguments: &[SMTVariable],
     ) -> Vec<SMTVariable> {
         assert_eq!(function.parameters.len(), arguments.len());
         for (param, arg) in function.parameters.iter().zip(arguments) {
@@ -163,7 +163,6 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
             self.evaluator.define_from_variable(&var, arg);
         }
 
-        let parameters = self.ssa_tracker.to_smt_variables(&function.parameters);
         self.encode_variable_declaration(&VariableDeclaration {
             variables: function.returns.clone(),
             value: None,