CONTRACTS: add doc for loop assigns inference #7774

	name: Build Linux partially with CPROVER tools

	on:
	pull_request:
	branches:
	- '**'

	jobs:
	# This job takes approximately 18 minutes
	CompileLinux:
	runs-on: ubuntu-20.04
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: true
	- name: Install Packages
	env:
	# This is needed in addition to -yq to prevent apt-get from asking for
	# user input
	DEBIAN_FRONTEND: noninteractive
	run: \|
	sudo apt-get update
	sudo apt-get install --no-install-recommends -y clang-10 clang++-10 flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache
	sudo apt-get install --no-install-recommends -y libssl-dev libelf-dev libudev-dev libpci-dev libiberty-dev autoconf
	sudo apt-get install --no-install-recommends -y gawk jq

	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-KERNEL
	restore-keys: \|
	${{ runner.os }}-20.04-make-clang-${{ github.ref }}
	${{ runner.os }}-20.04-make-clang
	- name: ccache environment
	run: \|
	echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
	echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
	- name: Zero ccache stats and limit in size
	run: ccache -z --max-size=500M
	- name: Build CBMC tools
	run: \|
	make -C src minisat2-download
	make -C src CXX='ccache /usr/bin/clang++' cbmc.dir goto-cc.dir goto-diff.dir -j4
	- name: Print ccache stats
	run: ccache -s

	- name: Run (Docker Based) Linux Build test
	run: integration/linux/compile_linux.sh

	- uses: actions/upload-artifact@v4
	with:
	name: CPROVER-faultyInput
	path: CPROVER/faultyInput/*

Provide feedback