// Path: src/main/java/gov/nasa/jpf/constraints/api/ConstraintSolver.java
// public abstract class ConstraintSolver {
//   
//   /**
//    * result returned by a constraint solver
//    * 
//    */
//   public static enum Result {SAT,UNSAT,DONT_KNOW};
//   
//   /**
//    * runs f by the constraint solver and returns if
//    * f can be satisfied
//    * 
//    * @param f formula to check for satisfiability
//    * @return the satisfiability {@link Result} 
//    */
//   public Result isSatisfiable(Expression<Boolean> f) {
//     return solve(f, new Valuation());
//   }
//   
//   
//   /**
//    * solves f and returns a satisfying solution
//    * 
//    * @param f 
//    * @param result solution that satisfies f or null in case of only checking for satisfiability
//    * @return the satisfiability {@link Result}
//    */
//   public abstract Result solve(Expression<Boolean> f, Valuation result);
// 
//   /**
//    * Create a solver context, which allows for incremental solving (i.e., via push and pop).
//    * This is an optional operation.
//    * @return a solver context
//    * @throws UnsupportedOperationException if the solver engine does not incremental solving
//    */
//   public SolverContext createContext() {
// 	  throw new UnsupportedOperationException("Solver does not support incremental solving");
//   }
//   
//   
//   // LEGACY API
//   
//   @Deprecated
//   public Result isSatisfiable(Expression<Boolean> f, MinMax m) {
//     return solve(f, m, new Valuation());
//   }
//   
//   @Deprecated
//   public Result solve(Expression<Boolean> f, MinMax m, Valuation val) {
//     //Expression<Boolean> mod = m.apply(f);
//     return solve(f, val);
//   }
//     
// }
// 
// Path: src/main/java/gov/nasa/jpf/constraints/exceptions/SolverCreationException.java
// public class SolverCreationException extends RuntimeException {
// 	private static final long serialVersionUID = 1L;
// 
// 	public SolverCreationException() {
// 	}
// 
// 	public SolverCreationException(String message) {
// 		super(message);
// 	}
// 
// 	public SolverCreationException(Throwable cause) {
// 		super(cause);
// 	}
// 
// 	public SolverCreationException(String message, Throwable cause) {
// 		super(message, cause);
// 	}
// 
// }


import gov.nasa.jpf.constraints.api.ConstraintSolver;
import gov.nasa.jpf.constraints.exceptions.SolverCreationException;
import java.lang.reflect.Constructor;
import java.lang.reflect.InvocationTargetException;
import java.util.Properties;
import java.util.logging.Level;
import java.util.logging.Logger;
			catch(NoSuchMethodException ex) {
				throw new IllegalArgumentException("Constraint solver class " + clazz.getName()
						+ " neither exposes Properties nor default constructor");
			}
			catch(SecurityException ex) {
				throw new IllegalArgumentException("Constraint solver class " + clazz.getName()
						+ " neither exposes Properties nor default constructor");
			}
		}
		
		this.ctor = ctor;
		this.hasPropertyCtor = hasPropertyCtor;
	}
	
	@Override
	public String[] getNames() {
		Class<?> declClazz = ctor.getDeclaringClass();
		return new String[]{declClazz.getSimpleName(), declClazz.getName()};
	}

	@Override
	public ConstraintSolver createSolver(Properties config) {
		try {
			if(hasPropertyCtor)
				return ctor.newInstance(config);
			logger.log(Level.FINE, "Note: {0} does not expose a " +
					"Properties constructor. No configuration is used.", ctor.getDeclaringClass().getName());
			return ctor.newInstance();
		}
		catch(IllegalAccessException ex) {
// Path: src/main/java/gov/nasa/jpf/constraints/api/ConstraintSolver.java
// public abstract class ConstraintSolver {
//   
//   /**
//    * result returned by a constraint solver
//    * 
//    */
//   public static enum Result {SAT,UNSAT,DONT_KNOW};
//   
//   /**
//    * runs f by the constraint solver and returns if
//    * f can be satisfied
//    * 
//    * @param f formula to check for satisfiability
//    * @return the satisfiability {@link Result} 
//    */
//   public Result isSatisfiable(Expression<Boolean> f) {
//     return solve(f, new Valuation());
//   }
//   
//   
//   /**
//    * solves f and returns a satisfying solution
//    * 
//    * @param f 
//    * @param result solution that satisfies f or null in case of only checking for satisfiability
//    * @return the satisfiability {@link Result}
//    */
//   public abstract Result solve(Expression<Boolean> f, Valuation result);
// 
//   /**
//    * Create a solver context, which allows for incremental solving (i.e., via push and pop).
//    * This is an optional operation.
//    * @return a solver context
//    * @throws UnsupportedOperationException if the solver engine does not incremental solving
//    */
//   public SolverContext createContext() {
// 	  throw new UnsupportedOperationException("Solver does not support incremental solving");
//   }
//   
//   
//   // LEGACY API
//   
//   @Deprecated
//   public Result isSatisfiable(Expression<Boolean> f, MinMax m) {
//     return solve(f, m, new Valuation());
//   }
//   
//   @Deprecated
//   public Result solve(Expression<Boolean> f, MinMax m, Valuation val) {
//     //Expression<Boolean> mod = m.apply(f);
//     return solve(f, val);
//   }
//     
// }
// 
// Path: src/main/java/gov/nasa/jpf/constraints/exceptions/SolverCreationException.java
// public class SolverCreationException extends RuntimeException {
// 	private static final long serialVersionUID = 1L;
// 
// 	public SolverCreationException() {
// 	}
// 
// 	public SolverCreationException(String message) {
// 		super(message);
// 	}
// 
// 	public SolverCreationException(Throwable cause) {
// 		super(cause);
// 	}
// 
// 	public SolverCreationException(String message, Throwable cause) {
// 		super(message, cause);
// 	}
// 
// }


// Path: src/main/java/gov/nasa/jpf/constraints/solvers/ReflectionSolverProvider.java
import gov.nasa.jpf.constraints.api.ConstraintSolver;
import gov.nasa.jpf.constraints.exceptions.SolverCreationException;
import java.lang.reflect.Constructor;
import java.lang.reflect.InvocationTargetException;
import java.util.Properties;
import java.util.logging.Level;
import java.util.logging.Logger;

			catch(NoSuchMethodException ex) {
				throw new IllegalArgumentException("Constraint solver class " + clazz.getName()
						+ " neither exposes Properties nor default constructor");
			}
			catch(SecurityException ex) {
				throw new IllegalArgumentException("Constraint solver class " + clazz.getName()
						+ " neither exposes Properties nor default constructor");
			}
		}
		
		this.ctor = ctor;
		this.hasPropertyCtor = hasPropertyCtor;
	}
	
	@Override
	public String[] getNames() {
		Class<?> declClazz = ctor.getDeclaringClass();
		return new String[]{declClazz.getSimpleName(), declClazz.getName()};
	}

	@Override
	public ConstraintSolver createSolver(Properties config) {
		try {
			if(hasPropertyCtor)
				return ctor.newInstance(config);
			logger.log(Level.FINE, "Note: {0} does not expose a " +
					"Properties constructor. No configuration is used.", ctor.getDeclaringClass().getName());
			return ctor.newInstance();
		}
		catch(IllegalAccessException ex) {
			throw new SolverCreationException(ex);