I got the following output:
----------- Config contents
branch_start = 1
cg.boolean.false_first = true
cg.break_single_choice = false
cg.enable_atomic = true
cg.enumerate_random = false
cg.max_processors = 1
cg.randomize_choices = NONE
cg.seed = 42
cg.threads.break_arrays = false
cg.threads.break_sleep = true
cg.threads.break_start = true
cg.threads.break_yield = true
classpath = /home/zzy/jpf/test
config = /home/zzy/jpf/test/Example.jpf
config_path = /home/zzy/jpf/test
extensions = /home/zzy/jpf/jpf-core,/home/zzy/jpf/jpf-symbc
jpf-core = /home/zzy/jpf/jpf-core
jpf-core.classpath = /home/zzy/jpf/jpf-core/build/jpf-classes.jar;/home/zzy/jpf/jpf-core/build/examples
jpf-core.native_classpath = /home/zzy/jpf/jpf-core/build/jpf.jar;/home/zzy/jpf/jpf-core/build/jpf-annotations.jar
jpf-core.peer_packages = gov.nasa.jpf.vm,<model>,<default>
jpf-core.sourcepath = /home/zzy/jpf/jpf-core/src/examples
jpf-core.test_classpath = /home/zzy/jpf/jpf-core/build/tests
jpf-symbc = /home/zzy/jpf/jpf-symbc
jpf-symbc.classpath = /home/zzy/jpf/jpf-symbc/build/jpf-symbc-classes.jar
jpf-symbc.native_classpath = /home/zzy/jpf/jpf-symbc/build/jpf-symbc.jar;/home/zzy/jpf/jpf-symbc/build/jpf-symbc-annotations.jar;/home/zzy/jpf/jpf-symbc/lib/choco-1_2_04.jar;/home/zzy/jpf/jpf-symbc/lib/choco-solver-2.1.1-20100709.142532-2.jar;/home/zzy/jpf/jpf-symbc/lib/STPJNI.jar;/home/zzy/jpf/jpf-symbc/lib/scale.jar;/home/zzy/jpf/jpf-symbc/lib/automaton.jar;/home/zzy/jpf/jpf-symbc/lib/iasolver.jar;/home/zzy/jpf/jpf-symbc/lib/string.jar;/home/zzy/jpf/jpf-symbc/lib/solver.jar;/home/zzy/jpf/jpf-symbc/lib/commons-lang-2.4.jar;/home/zzy/jpf/jpf-symbc/lib/commons-math-1.2.jar;/home/zzy/jpf/jpf-symbc/lib/coral.jar;/home/zzy/jpf/jpf-symbc/lib/opt4j-2.4.jar;/home/zzy/jpf/jpf-symbc/lib/libcvc3.jar;/home/zzy/jpf/jpf-symbc/lib/org.sat4j.core.jar;/home/zzy/jpf/jpf-symbc/lib/org.sat4j.pb.jar;/home/zzy/jpf/jpf-symbc/lib/aima-core.jar;/home/zzy/jpf/jpf-symbc/lib/yicesapijava.jar;/home/zzy/jpf/jpf-symbc/lib/PathConditionsReliability-0.0.1.jar;/home/zzy/jpf/jpf-symbc/lib/grappa.jar
jpf-symbc.test_classpath = build/tests
jpf.app = /home/zzy/jpf/test/Example.jpf
jpf.home = /home/zzy/jpf
jpf.print_exception_stack = true
jpf.site = /home/zzy/.jpf/site.properties
jvm.insn_factory.class = gov.nasa.jpf.jvm.bytecode.InstructionFactory
jvm.nested_init = false
jvm.nested_init.exclude = java.*,javax.*,sun.misc.*
listener = gov.nasa.jpf.symbc.SymbolicListener
listener.autoload = gov.nasa.jpf.NonNull,gov.nasa.jpf.Const
listener.gov.nasa.jpf.Const = gov.nasa.jpf.tools.ConstChecker
listener.gov.nasa.jpf.NonNull = gov.nasa.jpf.tools.NonNullChecker
log.handler.class = gov.nasa.jpf.util.LogHandler
log.level = warning
peer_packages = gov.nasa.jpf.symbc;
race.exclude = java.*,javax.*
report.class = gov.nasa.jpf.report.Reporter
report.console.class = gov.nasa.jpf.report.ConsolePublisher
report.console.constraint = constraint,snapshot
report.console.finished = result,statistics
report.console.probe = statistics
report.console.property_violation = error,snapshot
report.console.show_code = false
report.console.show_method = true
report.console.show_steps = true
report.console.start = jpf,sut
report.console.transition =
report.html.class = gov.nasa.jpf.report.HTMLPublisher
report.html.constraint = constraint
report.html.finished = result,statistics,error,snapshot,output
report.html.property_violation =
report.html.start = jpf,sut,platform,user,dtg,config
report.publisher = console
report.xml.class = gov.nasa.jpf.report.XMLPublisher
search.class = gov.nasa.jpf.search.DFSearch
search.heuristic.branch.count_early = true
search.heuristic.branch.no_branch_return = -1
search.heuristic.queue_limit = -1
search.match_depth = false
search.min_free = 1M
search.multiple_errors = true
search.properties = gov.nasa.jpf.vm.NotDeadlockedProperty,gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
sourcepath = /home/zzy/jpf/test
symbolic.dp = choco
symbolic.method = Example.foo(sym#con)
target = Example
test.report.console.finished = result
vm.backtracker.class = gov.nasa.jpf.vm.DefaultBacktracker
vm.boot_classpath = <system>
vm.class = gov.nasa.jpf.vm.SingleProcessVM
vm.classloader.class = gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo
vm.fields_factory.class = gov.nasa.jpf.vm.DefaultFieldsFactory
vm.finalize = false
vm.gc = true
vm.heap.class = gov.nasa.jpf.vm.OVHeap
vm.ignore_uncaught_handler = false
vm.max_alloc_gc = -1
vm.max_transition_length = 50000
vm.no_orphan_methods = false
vm.pass_uncaught_handler = true
vm.path_output = false
vm.process_finalizers = false
vm.restorer.class = .vm.DefaultMementoRestorer
vm.reuse_tid = false
vm.scheduler.class = gov.nasa.jpf.vm.DelegatingScheduler
vm.scheduler.sharedness.class = gov.nasa.jpf.vm.PathSharednessPolicy
vm.scheduler.sync.class = gov.nasa.jpf.vm.AllRunnablesSyncPolicy
vm.scheduler_factory.class = gov.nasa.jpf.vm.DefaultSchedulerFactory
vm.serializer.class = gov.nasa.jpf.vm.serialize.CFSerializer
vm.shared.break_on_exposure = true
vm.shared.never_break_fields = java.lang.Thread*.*,java.lang.System.*,java.lang.Runtime.*,java.lang.Boolean.*,java.lang.String.*,java.lang.*.TYPE,java.util.HashMap.EMPTY_TABLE,java.util.HashSet.PRESENT,java.util.concurrent.ThreadPoolExecutor*.*,java.util.concurrent.ThreadPoolExecutor*.*,java.util.concurrent.TimeUnit.*,java.util.concurrent.Exchanger.CANCEL,java.util.concurrent.Exchanger.NULL_ITEM,java.util.concurrent.Executors$DefaultThreadFactory.*,sun.misc.VM.*,sun.misc.SharedSecrets.*,sun.misc.Unsafe.theUnsafe,gov.nasa.jpf.util.test.TestJPF.*
vm.shared.never_break_methods = java.util.concurrent.ThreadPoolExecutor.processWorkerExit,java.util.concurrent.locks.Abstract*Synchronizer.*,java.util.concurrent.ThreadPoolExecutor.getTask,java.util.concurrent.atomic.Atomic*.*,java.util.concurrent.Exchanger.doExchange,java.util.concurrent.ThreadPoolExecutor.interruptIdleWorkers,java.util.concurrent.TimeUnit.*
vm.shared.never_break_types = java.util.concurrent.TimeUnit
vm.shared.skip_constructed_finals = false
vm.shared.skip_finals = true
vm.shared.skip_static_finals = false
vm.shared.sync_detection = true
vm.statics.class = gov.nasa.jpf.vm.OVStatics
vm.store_steps = false
vm.sysprop.source = SELECTED
vm.threadlist.class = gov.nasa.jpf.vm.ThreadList
vm.time.class = gov.nasa.jpf.vm.SystemTime
vm.tree_output = true
vm.untracked = true
vm.verify.ignore_path = true