jpf.properties

# project config for jpf-regression extension

jpf-memoise = ${config_path}

jpf-memoise.native_classpath=\
 ${jpf-memoise}/build/jpf-memoise.jar;\
 ${jpf-symbc}/lib/commons-lang-2.4.jar;
 
jpf-memoise.classpath=\
 ${jpf-memoise}/build/tests;\
 ${jpf-memoise}/build/examples;
  
peer_packages= gov.nasa.jpf.symbc,${peer_packages}

# The following JPF options are usually used for SPF as well:

# no state matching

vm.storage.class=nil

# instruct jpf not to stop at first error

search.multiple_errors=true

# specify the search strategy (default is DFS)

#search.class = .search.heuristic.BFSHeuristic

# limit the search depth (number of choices along the path)

#search.depth_limit = 10

#You can specify multiple methods to be executed symbolically as follows:
#symbolic.method=<list of methods to be executed symbolically separated by ",">

#You can pick which decision procedure to choose (if unspecified, choco is used as default):ss

#symbolic.dp=choco

#symbolic.dp=iasolver

#symbolic.dp=cvc3

#symbolic.dp=cvc3bitvec

#symbolic.dp=no_solver

#A new option was added to implement lazy initialization (see [TACAS'03] paper)
#symbolic.lazy=on

#(default is off) -- for now it is incompatible with Strings

#New options have been added, to specify min/max values for symbolic variables and also to give the default for don't care values.
#symbolic.minint=-100

#symbolic.maxint=100

#symbolic.minreal=-1000.0

#symbolic.maxreal=1000.0

#symbolic.undefined=0