bmc-concurrency.properties

# This file is part of CPAchecker,
# a tool for configurable software verification:
# https://cpachecker.sosy-lab.org
#
# SPDX-FileCopyrightText: 2007-2020 Dirk Beyer <https://www.sosy-lab.org>
#
# SPDX-License-Identifier: Apache-2.0

// ----------------------------------------------------------------------
// This configuration file enables BMC for verifying multi-threaded programs.
// ----------------------------------------------------------------------

#include includes/bmc.properties

#include includes/concurrency.properties

specification = specification/default.spc

#include includes/resource-limits.properties

CompositeCPA.cpas = cpa.threading.ThreadingCPA, \
                    cpa.predicate.PredicateCPA, \
                    cpa.assumptions.storage.AssumptionStorageCPA, \
                    cpa.loopbound.LoopBoundCPA, \
                    cpa.value.ValueAnalysisCPA

analysis.traversal.order = bfs
analysis.traversal.useReversePostorder          = false
analysis.traversal.useCallstack                 = false
analysis.traversal.useReverseLoopstack          = false
analysis.traversal.useReverseLoopIterationCount = false

# Number of threads should be irrelevant, but have a huge impact on performance.
analysis.traversal.useNumberOfThreads  = false

# prevent the stop-operator from aborting the stop-check early when it crosses a target state
cpa.arg.coverTargetStates = false

# the loop unrolling bound
cpa.loopbound.maxLoopIterations = 10

# enable stack-based tracking of loops
cpa.loopbound.trackStack = false

# Use merge^{JOIN} for value analysis alongside predicate to prevent unnecessary unrolling
cpa.value.merge = JOIN

counterexample.export.allowImpreciseCounterexamples=true