# This is the listener that can detect variable write-after-write conflicts
#listener=gov.nasa.jpf.listener.VariableConflictTracker
-#listener=gov.nasa.jpf.listener.StateReducer
-listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer
+listener=gov.nasa.jpf.listener.StateReducer
+#listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer
# Potentially conflicting variables
# Alarms
# Debug mode for StateReducer
debug_state_transition=true
+activate_state_reduction=true
# Timeout in minutes (default is 0 which means no timeout)
timeout=30
-#search.class = gov.nasa.jpf.search.heuristic.RandomHeuristic
+search.class = gov.nasa.jpf.search.heuristic.RandomHeuristic
+search.heuristic.beam_search=true
#search.class = gov.nasa.jpf.search.heuristic.UserHeuristic
#search.class = gov.nasa.jpf.search.heuristic.BFSHeuristic
#search.class = gov.nasa.jpf.search.heuristic.DFSHeuristic