# JPF properties to run the oldclassic example with DeadlockAnalyzer report

target=eShop.Client

report.console.property_violation=error,snapshot,trace

#symbolic.method=eShop.Client.main(sym#sym#sym)
symbolic.method= eShop.client.getPriceDiscount(sym)
symbolic.method= eShop.client.getPriceShippingPrice(sym)
classpath=${jpf-symbc}/build/examples/
sourcepath=${jpf-symbc}/src/examples/
symbolic.debug=true

listener = .symbc.SymbolicListener

#symbolic.collect_constraints=false
#symbolic.db=no_solver
symbolic.db=z3
symbolic.optimizechoices=false