Enforce subrange and refinement type restrictions on local constants #1439


	name: Kind2 CI

	on:
	pull_request:
	branches: [ develop ]
	push:
	branches: [ develop ]

	jobs:
	kind2-build:
	strategy:
	matrix:
	os: [ ubuntu-20.04, macos-12, macos-14 ]
	include:
	- os: macos-12
	pkg_update: brew update
	ocaml-version: 4.09.1
	- os: macos-14
	pkg_update: brew update
	ocaml-version: 4.10.2 # Oldest version available
	- os: ubuntu-20.04
	pkg_update: sudo apt-get update -y
	ocaml-version: 4.09.1

	runs-on: ${{ matrix.os }}

	steps:
	- name: Checkout code
	uses: actions/checkout@v4

	- name: Make OCaml warnings fatal
	run: \|
	head -n1 dune-project > dune-workspace
	echo '(profile strict)' >> dune-workspace

	- name: Update package information
	run: ${{ matrix.pkg_update }}

	- name: Build Kind 2
	uses: ./.github/actions/build-kind2
	with:
	ocaml-version: ${{ matrix.ocaml-version }}

	- name: Install Z3 (Ubuntu)
	if: runner.os == 'Linux'
	run: \|
	Z3_VERSION=4.12.2
	Z3_OS_VERSION=x64-glibc-2.31
	Z3_ZIP_NAME=z3-$Z3_VERSION-$Z3_OS_VERSION
	wget -q https://github.com/Z3Prover/z3/releases/download/z3-$Z3_VERSION/$Z3_ZIP_NAME.zip
	unzip -q $Z3_ZIP_NAME.zip
	sudo cp $Z3_ZIP_NAME/bin/z3 /usr/bin/

	- name: Install Z3 (macOS)
	if: runner.os == 'macOS'
	run: brew install z3

	- name: Install unit test dependencies
	run: opam install ounit2

	- name: Run ounit and regression tests
	run: opam exec make test

	- name: Upload kind2 artifact
	if: github.event_name == 'push' && github.ref == 'refs/heads/develop'
	uses: actions/upload-artifact@v4
	with:
	name: kind2-${{ matrix.os }}
	path: bin/kind2

Provide feedback