Welcome to GMC

Multi-Core Model Checking

Stateful classes in CIVL that may not be necessary to be stateful:
edu.udel.cis.vsl.civl.kripke.common.CommonEvaluator.java
boundVariableStack
originalState
originalPid
valueAtOrRemoteCount

Possible solution: spawn an EvaluatorWorker
edu.udel.cis.vsl.civl.semantics.common.CommonExecutor.java
numSteps
Possible solution: Each thread has its own copy of Executor.