combinations-valueCegar60+pred-cmc.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 uses a sequential combination of two
# analyses: the ValueAnalysisCPA with a maximum execution time of 60s
# and the Adjustable-Block Encoding CPA for predicate analysis.
# Combination is based on conditional model checking (CMC).
# First analysis generates an assumption describing which states cannot
# be verified. Second analysis uses the assumption to only verify the
# remaining non-verified program parts.
# ----------------------------------------------------------------------

# Use sequential combination of analyses.
analysis.restartAfterUnknown = true
restartAlgorithm.writeIntermediateOutputFiles = true

# The used analyses.
restartAlgorithm.configFiles = components/valueAnalysis-Cegar-60s-generate-cmc-condition.properties, components/predicateAnalysis-use-cmc-condition-nospec.properties

specification=specification/default.spc