### Install Z3 on macOS

Source: https://github.com/uclid-org/uclid/blob/master/README.md

Run this script from the root of the UCLID5 repository to download and set up Z3 binaries for macOS.

```bash
$ source get-z3-macos.sh
```

--------------------------------

### Install SBT on macOS

Source: https://github.com/uclid-org/uclid/blob/master/README.md

Install the Simple Build Tool (SBT) on macOS using Homebrew. This is only required if you plan to build Uclid from source.

```bash
brew install sbt
```

--------------------------------

### Install Delphi on Linux

Source: https://github.com/uclid-org/uclid/blob/master/README.md

Optional script to install Delphi binaries on Linux. Some CI synthesis tests may fail without Delphi.

```bash
$ source get-delphi-linux.sh
```

--------------------------------

### Install Delphi on macOS

Source: https://github.com/uclid-org/uclid/blob/master/README.md

Optional script to install Delphi binaries on macOS. Some CI synthesis tests may fail without Delphi.

```bash
$ source get-delphi-macos.sh
```

--------------------------------

### Define Initial Model States

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test69.txt

Examples of defining initial array states and integer constants using SMT-LIB define-fun syntax.

```SMT-LIB
(model
  (define-fun initial_26_numbers () (Array _type_tuple_1_ Int)
    (let ((a!1 (store (store (store ((as const (Array _type_tuple_1_ Int)) 10)
                                (_make__type_tuple_1_ true 8)
                                0)
                         (_make__type_tuple_1_ false 7)
                         0)
                  (_make__type_tuple_1_ true 5)
                  0)))
(let ((a!2 (store (store (store a!1 (_make__type_tuple_1_ true 9) 0)
                         (_make__type_tuple_1_ false 2)
                         (- 2))
                  (_make__type_tuple_1_ false 9)
                  0)))
(let ((a!3 (store (store (store a!2 (_make__type_tuple_1_ false 3) 0)
                         (_make__type_tuple_1_ true 3)
                         0)
                  (_make__type_tuple_1_ false 5)
                  0)))
(let ((a!4 (store (store (store a!3 (_make__type_tuple_1_ false 6) 0)
                         (_make__type_tuple_1_ false 1)
                         (- 1))
                  (_make__type_tuple_1_ true 2)
                  2)))
(let ((a!5 (store (store (store a!4 (_make__type_tuple_1_ false 0) 0)
                         (_make__type_tuple_1_ true 6)
                         0)
                  (_make__type_tuple_1_ true 0)
                  0)))
(let ((a!6 (store (store (store a!5 (_make__type_tuple_1_ false 4) 0)
                         (_make__type_tuple_1_ false 8)
                         0)
                  (_make__type_tuple_1_ true 4)
                  0)))
  (store (store a!6 (_make__type_tuple_1_ true 7) 0)
         (_make__type_tuple_1_ true 1)
         1))))))))
  (define-fun initial_16_index () Int
    0)
  (define-fun initial_27_sum () Int
    3)
  (define-fun initial_18_sum () Int
    0)
  (define-fun initial_21_sum () Int
    0)
  (define-fun initial_22_index () Int
    2)
  (define-fun initial_19_index () Int
    1)
  (define-fun initial_23_numbers () (Array _type_tuple_1_ Int)
    (let ((a!1 (store (store (store ((as const (Array _type_tuple_1_ Int)) 10)
                                (_make__type_tuple_1_ true 8)
                                0)
                         (_make__type_tuple_1_ false 7)
                         0)
                  (_make__type_tuple_1_ true 5)
                  0)))
(let ((a!2 (store (store (store a!1 (_make__type_tuple_1_ true 9) 0)
                         (_make__type_tuple_1_ false 9)
                         0)
                  (_make__type_tuple_1_ true 3)
                  0)))
(let ((a!3 (store (store (store a!2 (_make__type_tuple_1_ false 3) 0)
                         (_make__type_tuple_1_ false 2)
                         0)
                  (_make__type_tuple_1_ false 5)
                  0)))
(let ((a!4 (store (store (store a!3 (_make__type_tuple_1_ false 6) 0)
                         (_make__type_tuple_1_ false 1)
                         (- 1))
                  (_make__type_tuple_1_ true 6)
                  0)))
(let ((a!5 (store (store (store a!4 (_make__type_tuple_1_ false 0) 0)
                         (_make__type_tuple_1_ true 2)
                         0)
                  (_make__type_tuple_1_ true 0)
                  0)))
(let ((a!6 (store (store (store a!5 (_make__type_tuple_1_ false 4) 0)
                         (_make__type_tuple_1_ false 8)
                         0)
                  (_make__type_tuple_1_ true 4)
                  0)))
  (store (store a!6 (_make__type_tuple_1_ true 7) 0)
         (_make__type_tuple_1_ true 1)
         1))))))))
  (define-fun initial_24_sum () Int
    1)
  (define-fun initial_20_numbers () (Array _type_tuple_1_ Int)
    (let ((a!1 (store (store (store ((as const (Array _type_tuple_1_ Int)) 10)
                                (_make__type_tuple_1_ true 8)
                                0)
                         (_make__type_tuple_1_ false 7)
                         0)
                  (_make__type_tuple_1_ true 5)
                  0)))
(let ((a!2 (store (store (store a!1 (_make__type_tuple_1_ true 9) 0)
                         (_make__type_tuple_1_ false 9)
                         0)
                  (_make__type_tuple_1_ true 3)
                  0)))
(let ((a!3 (store (store (store a!2 (_make__type_tuple_1_ false 3) 0)
                         (_make__type_tuple_1_ false 2)
                         0)
                  (_make__type_tuple_1_ false 5)
                  0)))
(let ((a!4 (store (store (store a!3 (_make__type_tuple_1_ false 6) 0)
                         (_make__type_tuple_1_ true 6)
                         0)
                  (_make__type_tuple_1_ true 2)
                  0)))
(let ((a!5 (store (store (store a!4 (_make__type_tuple_1_ false 0) 0)
                         (_make__type_tuple_1_ false 1)
                         0)
                  (_make__type_tuple_1_ true 0)
                  0)))
(let ((a!6 (store (store (store a!5 (_make__type_tuple_1_ false 4) 0)
                         (_make__type_tuple_1_ false 8)
                         0)
                  (_make__type_tuple_1_ true 4)
                  0))))
```

--------------------------------

### Example of Commits to Squash

Source: https://github.com/uclid-org/uclid/blob/master/CONTRIBUTING.md

Example of commit history that should be squashed into a single meaningful commit during an interactive rebase.

```text
commit c76ef1e8bbfa1cb06f42dsdd3g02138002bca938 
Author: polgreen <epolgreen@gmail.com>
Date:   Tue Oct 27 15:12:03 2020 -0700

    fixes mistake in previous commit

commit 6502265e4a85688ff92d963419c1957ef3cb73b5
Author: polgreen <epolgreen@gmail.com>
Date:   Tue Oct 27 11:18:52 2020 -0700

    Add array reads to readset

    The redundant assignment eliminator was removing relevant assigns because
    it was failing to count array select statements as reads of the index variable, if the array select
    happens on the LHS of an assign. Bug exposed by test/test-redundant-assign.ucl
```

--------------------------------

### Install CVC5 on Linux

Source: https://github.com/uclid-org/uclid/blob/master/README.md

Optional script to install CVC5 binaries on Linux. Some CI synthesis tests may fail without CVC5.

```bash
$ source get-cvc5-linux.sh
```

--------------------------------

### Install Z3 on Linux

Source: https://github.com/uclid-org/uclid/blob/master/README.md

Run this script from the root of the UCLID5 repository to download and set up Z3 binaries for Linux. Ensure your PATH and LD_LIBRARY_PATH are updated.

```bash
$ source get-z3-linux.sh
```

--------------------------------

### Install CVC5 on macOS

Source: https://github.com/uclid-org/uclid/blob/master/README.md

Optional script to install CVC5 binaries on macOS. Some CI synthesis tests may fail without CVC5.

```bash
$ source get-cvc5-macos.sh
```

--------------------------------

### Install Java 11 with Homebrew on macOS

Source: https://github.com/uclid-org/uclid/blob/master/README.md

Recommended method for installing OpenJDK 11 on macOS using Homebrew. Ensure Java 11 is set as the default.

```bash
brew install openjdk@11
```

--------------------------------

### Run UCLID with a different SMT solver

Source: https://github.com/uclid-org/uclid/blob/master/README.md

Use the '-s' flag to specify an alternative backend SMT solver. This example shows how to use CVC5.

```bash
uclid examples/tutorial/ex1.1-fib-model.ucl -s "cvc5 --lang smt2 --produce-models"
```

--------------------------------

### Install Java 11 (Alternative) on macOS

Source: https://github.com/uclid-org/uclid/blob/master/README.md

Alternative method for installing Java 11 on older macOS versions using Homebrew. This involves tapping a specific cask.

```bash
brew update
brew tap homebrew/cask-versions
brew cask install java11
```

--------------------------------

### Uclid For and While Loops for Iteration

Source: https://context7.com/uclid-org/uclid/llms.txt

Demonstrates iteration using for loops over ranges and while loops with conditions and invariants. This example initializes arrays and calculates a sum within a loop.

```ucl
module main {
  var regs : [bv3]bv8;
  var sum : integer;

  define begin() : bv3 = 0bv3;
  define end()   : bv3 = 7bv3;

  init {
    // For loop with literal range
    for i in range(0bv3, 7bv3) {
      regs[i] = 1bv8;
    }

    // For loop with typed iterator and macro bounds
    for (j : bv3) in range(begin(), end()) {
      regs[j] = 0bv8;
    }

    // While loop with invariant
    sum = 0;
    var k : integer;
    k = 0;
    while (k < 10)
      invariant sum >= 0;
    {
      sum = sum + k;
      k = k + 1;
    }
  }
}
```

--------------------------------

### Define State: Initial

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test9.txt

Defines initial state values for various variables. Crucial for setting up the starting conditions of a model.

```smt
(define-fun initial_31___ucld_78___ucld_63_s3XX_pending_copy2 () Bool
    false)
```

```smt
(define-fun initial_29___ucld_75___ucld_51_s2XX_pending_copy2 () Bool
    false)
```

```smt
(define-fun initial_79___ucld_80___ucld_56_s3XX_pending_copy2 () Bool
    false)
```

```smt
(define-fun initial_26___ucld_66___ucld_9_s1X_pending_copy2 () Bool
    false)
```

```smt
(define-fun initial_4___ucld_76___ucld_47_s2XX_pending_copy2 () Bool
    false)
```

--------------------------------

### Uclid If-Else and Case Statements for Control Flow

Source: https://context7.com/uclid-org/uclid/llms.txt

Illustrates control flow using if-else and case statements for conditional logic. The example shows how to transition between traffic light states based on current state and a step counter.

```ucl
module main {
  type light_t = enum { red, yellow, green };

  procedure next_light(light : light_t, step : integer)
    returns (lightP : light_t, stepP: integer)
  {
    // If statement
    if (step == 0) {
      // Case statement
      case
        (light == green) : { 
          lightP = yellow;
          stepP = step;
        }
        (light == yellow) : {
          lightP = red;
          stepP = 2;
        }
        (light == red) : {
          lightP = green;
          stepP = 1;
        }
        default : {
          lightP = light;
          stepP = step;
        }
      esac
    } else {
      lightP = light;
      stepP = step - 1;
    }
  }
}
```

--------------------------------

### Define Initial Data Output

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test13.txt

Defines an initial integer value for data output. Represents a starting point for output values.

```smt-lib
(define-fun initial_236_data_out () Int
    0)

```

```smt-lib
(define-fun initial_133_data_out () Int
    0)

```

```smt-lib
(define-fun initial_281_data_out () Int
    0)

```

```smt-lib
(define-fun initial_207_data_out () Int
    0)

```

--------------------------------

### Define Initial Step Variable

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test15.txt

Defines the initial value for a step variable. This is used to set up the starting state of a model.

```smt
(define-fun initial_9___ucld_6_step_var () Int
    1)
```

```smt
(define-fun initial_1___ucld_6_step_var () Int
    2)
```

```smt
(define-fun initial_10___ucld_8_step_var () Int
    0)
```

```smt
(define-fun initial_2___ucld_8_step_var () Int
    1)
```

--------------------------------

### Define Initial Integer Tail Value

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test67.txt

Defines an initial integer value for a 'tail' variable. Used to set starting conditions.

```smt-lib
(define-fun initial_32_tail () Int
  2)
```

```smt-lib
(define-fun initial_42_tail () Int
  4)
```

```smt-lib
(define-fun initial_26_tail () Int
  0)
```

--------------------------------

### Define Initial Integer Tail Value (Variant)

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test67.txt

Defines an initial integer value for a 'tail' variable. Used to set starting conditions.

```smt-lib
(define-fun initial_52_tail () Int
  6)
```

--------------------------------

### Define Initial Light Unbound Output

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test15.txt

Defines the initial state of a light output. This is typically used to set the starting color or status of a light.

```smt
(define-fun initial_11___ucld_7_light_unbound_output () _type_enum_1_
    red)
```

```smt
(define-fun initial_12___ucld_5_light_unbound_output () _type_enum_1_
    green)
```

```smt
(define-fun initial_4___ucld_5_light_unbound_output () _type_enum_1_
    red)
```

```smt
(define-fun initial_3___ucld_7_light_unbound_output () _type_enum_1_
    green)
```

--------------------------------

### Execute UCLID5 from Command Line

Source: https://context7.com/uclid-org/uclid/llms.txt

Run verification models using various solver configurations and output options.

```bash
# Basic execution
uclid examples/tutorial/ex1.1-fib-model.ucl

# Print SMT file with prefix
uclid examples/tutorial/ex1.1-fib-model.ucl -g "output_prefix"

# Use alternative solver (CVC5)
uclid examples/tutorial/ex1.1-fib-model.ucl -s "cvc5 --lang smt2 --produce-models"

# Use SyGuS solver for synthesis
uclid examples/fib2safety-synth.ucl -y "cvc5 --lang=sygus2"
```

--------------------------------

### Uclid Init and Next Blocks for State Transition

Source: https://context7.com/uclid-org/uclid/llms.txt

Demonstrates initialization and state transition logic using parallel assignments with primed variables. The init block sets initial values, while the next block defines how the state changes.

```ucl
module main {
  type result_t = record { valid : boolean, value : bv8 };
  var regs : [bv3]bv8;
  var cnt  : bv8;
  output result : result_t;

  // Sequential assignments in init block
  init {
    // For loop for array initialization
    for i in range(0bv3, 7bv3) {
      regs[i] = 1bv8;
    }
    // Simultaneous assignment
    cnt, result.value = 1bv8, 1bv8;
  }

  // Parallel assignments in next block (note primed variables)
  next {
    // Call procedure and assign to primed output
    call (result') = exec_cmd();
    // Parallel assignment to primed state variable
    cnt' = Double(cnt);
  }
}
```

--------------------------------

### Instantiate Modules

Source: https://context7.com/uclid-org/uclid/llms.txt

Create hierarchical designs by instantiating modules and sharing inputs or comparing instance states.

```ucl
module common {
  type addr_t = bv8;
  type word_t = bv8;
  type mem_t = [addr_t]word_t;
}

module cpu {
  input imem : common.mem_t;
  var pc : common.addr_t;
  var dmem : common.mem_t;
  // ... cpu implementation
}

module main {
  type mem_t = common.mem_t;

  // Shared instruction memory
  var imem : mem_t;

  // Create two instances of the CPU module
  instance cpu_i_1 : cpu(imem : (imem));
  instance cpu_i_2 : cpu(imem : (imem));

  init { }

  next {
    // Invoke both CPU instances synchronously
    next (cpu_i_1);
    next (cpu_i_2);
  }

  // Properties comparing two instances
  invariant eq_pc : (cpu_i_1.pc == cpu_i_2.pc);
  invariant eq_mem : (forall (a : common.addr_t) :: cpu_i_1.dmem[a] == cpu_i_2.dmem[a]);

  control {
    bmc(3);
    check;
    print_results;
  }
}
```

--------------------------------

### Define Initial State

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test57.txt

Defines the initial boolean state of a system. Used to set up the starting conditions for verification.

```Uclid
(define-fun initial_48___ucld_37___ucld_10_eventually_C1_pending_copy2 () Bool
    false)
```

```Uclid
(define-fun initial_19___ucld_40___ucld_22_eventually_C2_pending_copy2 () Bool
    false)
```

```Uclid
(define-fun initial_18___ucld_34___ucld_6_st_var_copy2 () _type_enum_1_
    C1)
```

```Uclid
(define-fun initial_47___ucld_39___ucld_25_eventually_C2_pending_copy2 () Bool
    false)
```

```Uclid
(define-fun initial_2___ucld_36___ucld_13_eventually_C1_pending_copy2 () Bool
    false)
```

```Uclid
(define-fun initial_34___ucld_41___ucld_29_eventually_C2_pending_copy2 () Bool
    false)
```

--------------------------------

### Define Initial Mode (Variant 2)

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test63.txt

Sets the initial operating mode to 'normal_mode'.

```smt-lib
(define-fun initial_162_mode () _type_enum_1_
    normal_mode)
```

--------------------------------

### Define Initial Boolean State

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test66.txt

Defines an initial boolean state for a model. Use this to set up starting conditions for verification.

```smt-lib
(define-fun initial_24_initialized () Bool
    false)
```

```smt-lib
(define-fun initial_40_initialized () Bool
    true)
```

```smt-lib
(define-fun initial_29_value_found () Bool
    false)
```

```smt-lib
(define-fun initial_23_value_found () Bool
    false)
```

```smt-lib
(define-fun initial_39_value_found () Bool
    false)
```

```smt-lib
(define-fun initial_30_initialized () Bool
    true)
```

--------------------------------

### Define Initial Input Variable

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test33.txt

Defines an initial input variable in Uclid, representing values provided to the system at its start.

```smtlib
(define-fun initial_5___ucld_15___ucld_9_s_eq_n_plus_1_pending_copy2 () Bool
    false)
```

```smtlib
(define-fun input_3___ucld_16_main_copy_state_in () Bool
    false)
```

```smtlib
(define-fun input_4___ucld_16_main_copy_state_in () Bool
    false)
```

```smtlib
(define-fun input_5___ucld_16_main_copy_state_in () Bool
    false)
```

```smtlib
(define-fun initial_21___ucld_14___ucld_5_s_eq_n_pending_copy2 () Bool
    false)
```

--------------------------------

### Define Initial Mode (Variant 3)

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test63.txt

Sets the initial operating mode to 'normal_mode'.

```smt-lib
(define-fun initial_211_mode () _type_enum_1_
    normal_mode)
```

--------------------------------

### Define Initial Registers

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test63.txt

Initializes the register file. It uses an 'as-array' construct with a predefined array 'k!1464'.

```smtlib
(define-fun initial_196_regs () (Array regindex_t (_ BitVec 32))
    (_ as-array k!1464))
```

--------------------------------

### Define Initial Integer Variable

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test12.txt

Defines an integer variable with an initial value. Used for setting up the starting state of a model.

```smtlib
(define-fun initial_37_i () Int
  0)
```

```smtlib
(define-fun initial_22_x () Int
  0)
```

```smtlib
(define-fun initial_14_j () Int
  1)
```

```smtlib
(define-fun initial_32_j () Int
  0)
```

```smtlib
(define-fun initial_31_y () Int
  0)
```

```smtlib
(define-fun initial_39_j () Int
  1)
```

```smtlib
(define-fun initial_15_x () Int
  0)
```

```smtlib
(define-fun initial_13_y () Int
  0)
```

```smtlib
(define-fun initial_12_i () Int
  0)
```

```smtlib
(define-fun initial_46_j () Int
  2)
```

```smtlib
(define-fun initial_29_x () Int
  0)
```

```smtlib
(define-fun initial_16_i () Int
  (- 3))
```

```smtlib
(define-fun initial_11_x () Int
  0)
```

```smtlib
(define-fun initial_44_i () Int
  1)
```

```smtlib
(define-fun initial_38_y () Int
  0)
```

```smtlib
(define-fun initial_45_y () Int
  0)
```

```smtlib
(define-fun initial_43_x () Int
  0)
```

```smtlib
(define-fun initial_36_x () Int
  0)
```

```smtlib
(define-fun initial_18_j () Int
  (- 2))
```

```smtlib
(define-fun initial_23_i () Int
  (- 2))
```

```smtlib
(define-fun initial_24_y () Int
  0)
```

```smtlib
(define-fun initial_17_y () Int
  0)
```

--------------------------------

### Execute Inductive Proofs

Source: https://context7.com/uclid-org/uclid/llms.txt

Use induction for unbounded verification and debug failures using counterexample printing.

```ucl
module main {
  var a, b : integer;

  init {
    a = 0;
    b = 1;
  }

  next {
    a', b' = b, a + b;
  }

  // Strengthened inductive invariants
  invariant a_le_b: a <= b;
  invariant a_b_ge_0: (a >= 0 && b >= 0);

  control {
    // Inductive proof
    vobj = induction;
    check;
    print_results;

    // Print counterexample if proof fails
    vobj.print_cex(a, b);
  }
}
```

--------------------------------

### Define Initial State in Uclid

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test8.txt

Defines an initial state for a Uclid program. This is crucial for setting up the starting conditions of a verification or simulation.

```Uclid
(define-fun initial_91___ucld_74___ucld_32_s1XX_pending_copy2 () Bool
    false)
```

```Uclid
(define-fun initial_75___ucld_67___ucld_5_s1X_pending_copy2 () Bool
    false)
```

--------------------------------

### Define Initial Mode

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test63.txt

Sets the initial operating mode to 'normal_mode'.

```smt-lib
(define-fun initial_200_mode () _type_enum_1_
    normal_mode)
```

--------------------------------

### Define Initial Mode (Variant)

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test63.txt

Sets the initial operating mode to 'normal_mode'.

```smt-lib
(define-fun initial_155_mode () _type_enum_1_
    normal_mode)
```

--------------------------------

### SMT-LIB State and Input Definitions

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test43.txt

A series of SMT-LIB function definitions defining system states, inputs, and initial values for verification models.

```smtlib
(define-fun state_9___ucld_21_s_eq_n_plus_1_PENDING () Bool
    false)
  (define-fun input_4___ucld_16_main_copy_state_in () Bool
    false)
  (define-fun state_5___ucld_12_s_copy2 () (_ BitVec 8)
    #x20)
  (define-fun state_4___ucld_3_s_eq_n_z () Bool
    false)
  (define-fun state_6___ucld_17_main_state_copied () Bool
    false)
  (define-fun input_6___ucld_16_main_copy_state_in () Bool
    false)
  (define-fun havoc_62___ucld_4_s_eq_n_z () Bool
    false)
  (define-fun state_7___ucld_4_s_eq_n_z () Bool
    false)
  (define-fun state_2___ucld_3_s_eq_n_z () Bool
    false)
  (define-fun state_5___ucld_26_main_is_init () Bool
    false)
  (define-fun initial_7___ucld_13_b_copy2 () Bool
    true)
  (define-fun state_1___ucld_10_s_eq_n_plus_1_accept () Bool
    true)
  (define-fun state_9___ucld_26_main_is_init () Bool
    false)
  (define-fun state_12___ucld_26_main_is_init () Bool
    false)
  (define-fun state_3___ucld_11_n_copy2 () (_ BitVec 8)
    #x40)
  (define-fun state_5___ucld_3_s_eq_n_z () Bool
    false)
  (define-fun state_8___ucld_14___ucld_5_s_eq_n_pending_copy2 () Bool
    false)
  (define-fun state_13___ucld_14___ucld_5_s_eq_n_pending_copy2 () Bool
    true)
  (define-fun state_5___ucld_4_s_eq_n_z () Bool
    false)
  (define-fun state_6___ucld_11_n_copy2 () (_ BitVec 8)
    #x40)
  (define-fun state_3___ucld_7_s_eq_n_plus_1_z () Bool
    false)
  (define-fun state_12___ucld_24___ucld_10_s_eq_n_plus_1_accept_HAS_ACCEPTED () Bool
    true)
  (define-fun state_9___ucld_8_s_eq_n_plus_1_z () Bool
    false)
  (define-fun state_4___ucld_14___ucld_5_s_eq_n_pending_copy2 () Bool
    false)
  (define-fun state_5___ucld_8_s_eq_n_plus_1_z () Bool
    false)
  (define-fun state_10___ucld_22___ucld_6_s_eq_n_accept_HAS_ACCEPTED () Bool
    false)
  (define-fun state_2_n () (_ BitVec 8)
    #x04)
  (define-fun state_13___ucld_12_s_copy2 () (_ BitVec 8)
    #x16)
  (define-fun state_4___ucld_6_s_eq_n_accept () Bool
    false)
  (define-fun state_7___ucld_17_main_state_copied () Bool
    false)
  (define-fun state_8___ucld_24___ucld_10_s_eq_n_plus_1_accept_HAS_ACCEPTED () Bool
    false)
  (define-fun state_14___ucld_11_n_copy2 () (_ BitVec 8)
    #x16)
  (define-fun havoc_111___ucld_3_s_eq_n_z () Bool
    false)
  (define-fun havoc_104___ucld_4_s_eq_n_z () Bool
    false)
  (define-fun state_2___ucld_15___ucld_9_s_eq_n_plus_1_pending_copy2 () Bool
    false)
  (define-fun initial_23___ucld_11_n_copy2 () (_ BitVec 8)
    #x40)
  (define-fun state_11___ucld_8_s_eq_n_plus_1_z () Bool
    false)
  (define-fun state_8___ucld_12_s_copy2 () (_ BitVec 8)
    #x20)
  (define-fun havoc_64___ucld_8_s_eq_n_plus_1_z () Bool
    false)
  (define-fun state_13___ucld_17_main_state_copied () Bool
    true)
  (define-fun state_5___ucld_20_s_eq_n_PENDING () Bool
    true)
  (define-fun state_8___ucld_21_s_eq_n_plus_1_PENDING () Bool
    false)
  (define-fun state_11___ucld_5_s_eq_n_pending () Bool
    true)
  (define-fun state_13___ucld_13_b_copy2 () Bool
    false)
  (define-fun state_14___ucld_20_s_eq_n_PENDING () Bool
    true)
  (define-fun state_6___ucld_8_s_eq_n_plus_1_z () Bool
    false)
  (define-fun state_5___ucld_15___ucld_9_s_eq_n_plus_1_pending_copy2 () Bool
    false)
  (define-fun state_8___ucld_25_s_eq_n_plus_1_HAS_ACCEPTED_TRACE () Bool
    false)
  (define-fun state_4___ucld_25_s_eq_n_plus_1_HAS_ACCEPTED_TRACE () Bool
    false)
  (define-fun state_2___ucld_9_s_eq_n_plus_1_pending () Bool
    false)
  (define-fun state_4___ucld_20_s_eq_n_PENDING () Bool
    true)
  (define-fun state_8___ucld_6_s_eq_n_accept () Bool
    false)
  (define-fun state_13___ucld_23_s_eq_n_HAS_ACCEPTED_TRACE () Bool
    false)
  (define-fun havoc_112___ucld_8_s_eq_n_plus_1_z () Bool
    false)
  (define-fun state_2_s () (_ BitVec 8)
    #x04)
  (define-fun state_8___ucld_3_s_eq_n_z () Bool
    false)
  (define-fun state_9___ucld_17_main_state_copied () Bool
    false)
  (define-fun state_9___ucld_5_s_eq_n_pending () Bool
    true)
  (define-fun state_2___ucld_11_n_copy2 () (_ BitVec 8)
    #x40)
  (define-fun state_14_s () (_ BitVec 8)
    #x1c)
  (define-fun state_14___ucld_12_s_copy2 () (_ BitVec 8)
    #x16)
  (define-fun state_13___ucld_7_s_eq_n_plus_1_z () Bool
    false)
  (define-fun state_10___ucld_9_s_eq_n_plus_1_pending () Bool
    false)
  (define-fun state_1___ucld_11_n_copy2 () (_ BitVec 8)
    #x40)
  (define-fun havoc_87___ucld_3_s_eq_n_z () Bool
    false)
  (define-fun state_12___ucld_5_s_eq_n_pending () Bool
    true)
  (define-fun state_10___ucld_8_s_eq_n_plus_1_z () Bool
    false)
  (define-fun state_2___ucld_25_s_eq_n_plus_1_HAS_ACCEPTED_TRACE () Bool
    false)
  (define-fun state_12___ucld_17_main_state_copied () Bool
    true)
  (define-fun state_2___ucld_22___ucld_6_s_eq_n_accept_HAS_ACCEPTED () Bool
    false)
  (define-fun state_12_n () (_ BitVec 8)
    #x18)
  (define-fun state_7___ucld_13_b_copy2 () Bool
    true)
  (define-fun havoc_100___ucld_8_s_eq_n_plus_1_z () Bool
    false)
```

--------------------------------

### Define Initial Integer Tail Value

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test11.txt

Defines an initial integer value for a 'tail' variable. Used to set starting conditions.

```smt
(define-fun initial_32_tail () Int
  2)
```

```smt
(define-fun initial_52_tail () Int
  6)
```

```smt
(define-fun initial_62_tail () Int
  8)
```

```smt
(define-fun initial_72_tail () Int
  10)
```

```smt
(define-fun initial_42_tail () Int
  4)
```

```smt
(define-fun initial_26_tail () Int
  0)
```

--------------------------------

### Define Initial State Value

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test3.txt

Use this to define the initial value for a state variable that is an enumerated type. This example initializes a state to 's1'.

```smt-lib
(define-fun initial_43___ucld_65_state_copy2 () _type_enum_1_
    s1)
```

--------------------------------

### Define Initial Integer Value

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test65.txt

Defines an initial integer value for a variable. Used to set the starting state of integer variables in the model.

```smt-lib
(define-fun initial_32_tail () Int
    2)
```

```smt-lib
(define-fun initial_26_tail () Int
    0)
```

--------------------------------

### Define Initial Boolean Value

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test65.txt

Defines an initial boolean value for a variable. Used to set the starting state of boolean variables in the model.

```smt-lib
(define-fun initial_24_initialized () Bool
    false)
```

```smt-lib
(define-fun initial_29_value_found () Bool
    false)
```

```smt-lib
(define-fun initial_23_value_found () Bool
    false)
```

```smt-lib
(define-fun initial_30_initialized () Bool
    true)
```

--------------------------------

### Define Initial State Functions

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test16.txt

Initializes step variables and light output states using define-fun declarations within a model block.

```lisp
(model 
  (define-fun initial_18___ucld_8_step_var () Int
    1)
  (define-fun initial_22___ucld_8_step_var () Int
    0)
  (define-fun initial_25___ucld_6_step_var () Int
    0)
  (define-fun initial_46___ucld_8_step_var () Int
    1)
  (define-fun initial_43___ucld_7_light_unbound_output () _type_enum_1_
    red)
  (define-fun initial_29___ucld_6_step_var () Int
    1)
  (define-fun initial_23___ucld_7_light_unbound_output () _type_enum_1_
    red)
  (define-fun initial_24___ucld_5_light_unbound_output () _type_enum_1_
    green)
  (define-fun initial_42___ucld_8_step_var () Int
    0)
  (define-fun initial_48___ucld_5_light_unbound_output () _type_enum_1_
    yellow)
  (define-fun initial_26___ucld_8_step_var () Int
    1)
  (define-fun initial_19___ucld_7_light_unbound_output () _type_enum_1_
    red)
  (define-fun initial_28___ucld_5_light_unbound_output () _type_enum_1_
    yellow)
  (define-fun initial_20___ucld_5_light_unbound_output () _type_enum_1_
    green)
  (define-fun initial_17___ucld_6_step_var () Int
    1)
  (define-fun initial_21___ucld_6_step_var () Int
    0)
  (define-fun initial_34___ucld_8_step_var () Int
    0)
  (define-fun initial_37___ucld_6_step_var () Int
    1)
  (define-fun initial_38___ucld_8_step_var () Int
    1)
  (define-fun initial_31___ucld_7_light_unbound_output () _type_enum_1_
    green)
  (define-fun initial_32___ucld_5_light_unbound_output () _type_enum_1_
    red)
  (define-fun initial_27___ucld_7_light_unbound_output () _type_enum_1_
    green)
  (define-fun initial_35___ucld_7_light_unbound_output () _type_enum_1_
    yellow)
  (define-fun initial_45___ucld_6_step_var () Int
    0)
  (define-fun initial_40___ucld_5_light_unbound_output () _type_enum_1_
    green)
  (define-fun initial_44___ucld_5_light_unbound_output () _type_enum_1_
    green)
  (define-fun initial_47___ucld_7_light_unbound_output () _type_enum_1_
    green)
  (define-fun initial_41___ucld_6_step_var () Int
    0)
  (define-fun initial_30___ucld_8_step_var () Int
    0)
  (define-fun initial_36___ucld_5_light_unbound_output () _type_enum_1_
    red)
  (define-fun initial_33___ucld_6_step_var () Int
    0)
  (define-fun initial_39___ucld_7_light_unbound_output () _type_enum_1_
    red)
)
```

--------------------------------

### Uclid Initial State Definition

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test22.txt

This function defines the initial state for a specific part of the Uclid model. It is used to set up the starting conditions for verification.

```smt
(model 
  (define-fun initial_19___ucld_2_if_star () Bool
    false)
)
```

--------------------------------

### Define Initial Data Memory State (Variant 2)

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test63.txt

Initializes the data memory array with specific values for certain addresses.

```smt-lib
(define-fun initial_208_dmem () (Array addr_t (_ BitVec 32))
    (lambda ((x!1 addr_t))
  (ite (= x!1 addr_t!val!6)
       #x00008000
       (ite (= x!1 addr_t!val!5) #x00000000 #x00000400))))
```

--------------------------------

### Build Universal Package with SBT

Source: https://github.com/uclid-org/uclid/blob/master/README.md

Command to build a universal package of Uclid using SBT after successful compilation and testing. This package contains the uclid binary.

```bash
sbt universal:packageBin
```

--------------------------------

### Define Initial Integer Variable with Negative Value

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test12.txt

Defines an integer variable with a negative initial value. This is used for setting up specific starting conditions in the model.

```smtlib
(define-fun initial_25_j () Int
  (- 1))
```

```smtlib
(define-fun initial_30_i () Int
  (- 1))
```

--------------------------------

### Define State: Main Initialization

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test9.txt

Defines a state variable 'main_is_init' to track the initialization status of the main component. Essential for ensuring proper startup.

```smt
(define-fun state_2___ucld_107_main_is_init () Bool
    false)
```

--------------------------------

### Uclid Invariants and Properties for Safety Specifications

Source: https://context7.com/uclid-org/uclid/llms.txt

Defines safety properties using invariant and property keywords. This example specifies that variable 'a' is always less than or equal to 'b', and that both 'a' and 'b' are non-negative.

```ucl
module main {
  var a, b : integer;

  init {
    a = 0;
    b = 1;
  }

  next {
    a', b' = b, a + b;
  }

  // Named invariant
  invariant a_le_b: a <= b;

  // Multiple invariants for stronger inductive argument
  invariant a_b_ge_0: (a >= 0 && b >= 0);

  // Property keyword is synonym for invariant
  property positive_sum: a + b > 0;
}
```

--------------------------------

### Define Initial Instruction Value (Variant 3)

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test63.txt

Sets an initial value for an instruction.

```smt-lib
(define-fun initial_201_inst () (_ BitVec 32)
    #x00000000)
```

--------------------------------

### Define Initial Program Counter (Variant 2)

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test63.txt

Sets the initial value of the program counter to a specific address.

```smt-lib
(define-fun initial_160_pc () addr_t
    addr_t!val!3)
```

--------------------------------

### Set Java 11 as Default on macOS

Source: https://github.com/uclid-org/uclid/blob/master/README.md

Configure your dotfiles (e.g., .bash_profile or .zshrc) to set JAVA_HOME to Java 11 and create an alias for convenience.

```bash
export JAVA_11_HOME=$(/usr/libexec/java_home -v11)
alias java11='export JAVA_HOME=$JAVA_11_HOME'
java11
```

--------------------------------

### Define Initial Program Counter

Source: https://github.com/uclid-org/uclid/blob/master/test/parser/command-response/output/parser_test63.txt

Defines the initial value for the program counter (PC), setting it to a specific address.

```smtlib
(define-fun initial_153_pc () addr_t
    addr_t!val!3)
```

--------------------------------

### Uclid Array Operations

Source: https://context7.com/uclid-org/uclid/llms.txt

Shows how to perform array select (read) and update (write) operations, including initializing arrays with quantified assumptions. Supports multi-dimensional arrays.

```ucl
module main {
  type addr_t = bv8;
  type word_t = bv32;

  var mem : [addr_t]word_t;
  var addr : addr_t;
  var data : word_t;

  init {
    // Initialize all array elements with quantified assumption
    assume (forall (a : addr_t) :: mem[a] == 0bv32);
    addr = 0bv8;
  }

  next {
    // Array select (read)
    data' = mem[addr];

    // Array update (write) with functional syntax
    mem' = mem[addr -> data + 1bv32];

    // Multi-dimensional array select
    // val = arr[i, j];

    // Multi-dimensional update
    // arr' = arr[i, j -> val];

    addr' = addr + 1bv8;
  }
}
```

--------------------------------

### Run a UCLID model

Source: https://github.com/uclid-org/uclid/blob/master/README.md

Execute a UCLID model using the 'uclid' command. This is the basic command to run any UCLID file.

```bash
$ uclid examples/tutorial/ex1.1-fib-model.ucl
```