failed to run `@example` block in src/example_bv_lcg.md:21-35 ```@example transitions = BoolExpr[states[i+1] == states[i] * 214013+2531011 for i=1:9] remainders = BoolExpr[ output_prev == urem(( states[1] >> 16 ) & 0x7FFF, 100), urem(( states[2] >> 16) & 0x7FFF, 100) == 29, urem(( states[3] >> 16) & 0x7FFF, 100) == 74, urem(( states[4] >> 16) & 0x7FFF, 100) == 95, urem(( states[5] >> 16) & 0x7FFF, 100) == 98, urem(( states[6] >> 16) & 0x7FFF, 100) == 40, urem(( states[7] >> 16) & 0x7FFF, 100) == 23, urem(( states[8] >> 16) & 0x7FFF, 100) == 58, urem(( states[9] >> 16) & 0x7FFF, 100) == 61, output_next == urem(( states[10] >> 16) & 0x7FFF, 100), ] ``` value = UndefVarError: `BoolExpr` not defined

failed to run `@example` block in src/example_bv_lcg.md:36-48 ```@example expr = and(all(transitions), all(remainders)) status = sat!(expr, solver=CVC5()) println("status = $status") for (i,state) in enumerate(states) println("state $i = $(value(state))") end # According to SAT/SMT By Example the previous output is 37 and the next output is 17. println("prev = $(value(output_prev))") println("next = $(value(output_next))") ``` value = UndefVarError: `transitions` not defined

failed to run `@example` block in src/example_job_shop.md:28-30 ```@example working_hours = all(and.(t1 .>= 0, t2 .+ d2 .<= 8)) ``` value = UndefVarError: `and` not defined suggestion: Use `&&` for short-circuiting boolean AND.

failed to run `@example` block in src/example_job_shop.md:33-35 ```@example sequencing = and(t2 .>= t1 .+ d1) ``` value = UndefVarError: `t2` not defined

failed to run `@example` block in src/example_job_shop.md:38-42 ```@example overlaps = [(1,2), (1,3), (2,3)] overlap_1 = all([or( t1[i] >= t1[j] + d1[j], t1[j] >= t1[i] + d1[i]) for (i,j) in overlaps]) overlap_2 = all([or( t2[i] >= t2[j] + d2[j], t2[j] >= t2[i] + d2[i]) for (i,j) in overlaps]) ``` value = UndefVarError: `t1` not defined

failed to run `@example` block in src/example_job_shop.md:45-52 ```@example status = sat!(working_hours, sequencing, overlap_1, overlap_2, solver=Z3()) println("status = $status") if status == :SAT println("t1 = $(value(t1))") println("t2 = $(value(t2))") end ``` value = UndefVarError: `Z3` not defined

failed to run `@example` block in src/example_scheduling.md:41-43 ```@example unavailability = and(¬A_bar .⟹ ¬A) ``` value = UndefVarError: `⟹` not defined

failed to run `@example` block in src/example_scheduling.md:46-52 ```@example M = [and(A[index_sets[j], t]) for j=1:J, t=1:T] # get a list of conflicts conflicts = [filter((i) -> i != j && length(intersect(index_sets[j], index_sets[i])) > 0, 1:J) for j=1:J ] no_double_booking = all([M[j,t] ⟹ ¬or(M[conflicts[j],t]) for j=1:J, t=1:T]) ``` value = UndefVarError: `J` not defined

failed to run `@example` block in src/example_scheduling.md:55-57 ```@example require_one_time = and(or(M[j,:]) for j=1:J) ``` value = UndefVarError: `J` not defined