invariantGeneration-incremental.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

// Configuration for incremental creation of light-weight invariants
// (invariants that might not be sufficient for proving program safety,
// but can help other analyses) based on a data-flow analysis.
// This configuration is intended as helper for other analyses
// that can make use of such invariants.
// This configuration incrementally refines its precision
// until it can prove the program safe or it reaches the maximum precision.

#include includes/resource-limits.properties
specification = specification/default.spc

analysis.useParallelAnalyses = true
parallelAlgorithm.configFiles = components/invariantGeneration.properties::supply-reached-refinable