code: def test_random_problems():
      z3 = import_module("z3")
      if z3 is None:
          skip("z3 is not installed")
  
      special_cases = []
      x1, x2, x3 = symbols("x1 x2 x3")
      special_cases.append(
          [
              x1 - 3 * x2 <= -5,
              6 * x1 + 4 * x2 <= 0,
              -7 * x1 + 3 * x2 <= 3,
          ]
      )
      special_cases.append([-3 * x1 >= 3, Eq(4 * x1, -1)])
      special_cases.append([-4 * x1 < 4, 6 * x1 <= -6])
      special_cases.append([-3 * x2 >= 7, 6 * x1 <= -5, -3 * x2 <= -4])
      special_cases.append([x + y >= 2, x + y <= 1])
      special_cases.append(
          [x >= 0, x + y <= 2, x + 2 * y - z >= 6]
      )  # from paper example
      special_cases.append(
          [-2 * x1 - 2 * x2 >= 7, -9 * x1 >= 7, -6 * x1 >= 5]
      )
      special_cases.append([2 * x1 > -3, -9 * x1 < -6, 9 * x1 <= 6])
      special_cases.append([-2 * x1 < -4, 9 * x1 > -9])
      special_cases.append(
          [
              -6 * x1 >= -1,
              -8 * x1 + x2 >= 5,
              -8 * x1 + 7 * x2 < 4,
              x1 > 7,
          ]
      )
      special_cases.append(
          [
              Eq(x1, 2),
              Eq(5 * x1, -2),
              Eq(-7 * x2, -6),
              Eq(9 * x1 + 10 * x2, 9),
          ]
      )
      special_cases.append(
          [
              Eq(3 * x1, 6),
              Eq(x1 - 8 * x2, -9),
              Eq(-7 * x1 + 5 * x2, 3),
              Eq(3 * x2, 7),
          ]
      )
      special_cases.append([-4 * x1 < 4, 6 * x1 <= -6])
      special_cases.append(
          [
              -3 * x1 + 8 * x2 >= -8,
              -10 * x2 > 9,
              8 * x1 - 4 * x2 < 8,
              10 * x1 - 9 * x2 >= -9,
          ]
      )
      special_cases.append(
          [
              x1 + 5 * x2 >= -6,
              9 * x1 - 3 * x2 >= -9,
              6 * x1 + 6 * x2 < -10,
              -3 * x1 + 3 * x2 < -7,
          ]
      )
      special_cases.append(
          [
              -9 * x1 < 7,
              -5 * x1 - 7 * x2 < -1,
              3 * x1 + 7 * x2 > 1,
              -6 * x1 - 6 * x2 > 9,
          ]
      )
      special_cases.append(
          [
              9 * x1 - 6 * x2 >= -7,
              9 * x1 + 4 * x2 < -8,
              -7 * x2 <= 1,
              10 * x2 <= -7,
          ]
      )
  
      feasible_count = 0
      for i in range(50):
          if i % 8 == 0:
              constraints = make_random_problem(
                  num_variables=1, num_constraints=2, rational=False
              )
          elif i % 8 == 1:
              constraints = make_random_problem(
                  num_variables=2,
                  num_constraints=4,
                  rational=False,
                  disable_equality=True,
                  disable_nonstrict=True,
              )
          elif i % 8 == 2:
              constraints = make_random_problem(
                  num_variables=2,
                  num_constraints=4,
                  rational=False,
                  disable_strict=True,
              )
          elif i % 8 == 3:
              constraints = make_random_problem(
                  num_variables=3, num_constraints=12, rational=False
              )
          else:
              constraints = make_random_problem(
                  num_variables=3, num_constraints=6, rational=False
              )
  
          if i < len(special_cases):
              constraints = special_cases[i]
  
          if False in constraints or True in constraints:
              continue
  
          phi = And(*constraints)
          if phi == False:
              continue
          cnf = CNF.from_prop(phi)
          enc = EncodedCNF()
          enc.from_cnf(cnf)
          assert all(0 not in clause for clause in enc.data)
  
          lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
          s_subs = lra.s_subs
  
          lra.run_checks = True
          s_subs_rev = {value: key for key, value in s_subs.items()}
          lits = {lit for clause in enc.data for lit in clause}
  
          bounds = [
              (lra.enc_to_boundary[l], l)
              for l in lits
              if l in lra.enc_to_boundary
          ]
          bounds = sorted(
              bounds,
              key=lambda x: (
                  str(x[0].var),
                  x[0].bound,
                  str(x[0].upper),
              ),
          )  # to remove nondeterminism
  
          for b, l in bounds:
              if lra.result and lra.result[0] == False:
                  break
              lra.assert_lit(l)
  
          feasible = lra.check()
  
          if feasible[0] == True:
              feasible_count += 1
              assert check_if_satisfiable_with_z3(constraints) is True
              cons_funcs = [cons.func for cons in constraints]
              assignment = feasible[1]
              assignment = {
                  key.var: value for key, value in assignment.items()
              }
              if not (
                  StrictLessThan in cons_funcs
                  or StrictGreaterThan in cons_funcs
              ):
                  assignment = {
                      key: value[0] for key, value in assignment.items()
                  }
                  for cons in constraints:
                      assert cons.subs(assignment) == True
  
              else:
                  rat_assignment = find_rational_assignment(
                      constraints, assignment
                  )
                  assert rat_assignment is not None
          else:
              assert check_if_satisfiable_with_z3(constraints) is False
  
              conflict = feasible[1]
              assert len(conflict) >= 2
              conflict = {
                  lra.enc_to_boundary[-l].get_inequality()
                  for l in conflict
              }
              conflict = {
                  clause.subs(s_subs_rev) for clause in conflict
              }
              assert check_if_satisfiable_with_z3(conflict) is False
  
              # check that conflict clause is probably minimal
              for subset in itertools.combinations(
                  conflict, len(conflict) - 1
              ):
                  assert check_if_satisfiable_with_z3(subset) is True
  
imports: from sympy.core.numbers import Rational, I, oo
  from sympy.core.relational import Eq
  from sympy.core.symbol import symbols
  from sympy.core.singleton import S
  from sympy.matrices.dense import Matrix
  from sympy.matrices.dense import randMatrix
  from sympy.assumptions.ask import Q
  from sympy.logic.boolalg import And
  from sympy.abc import x, y, z
  from sympy.assumptions.cnf import CNF, EncodedCNF
  from sympy.functions.elementary.trigonometric import cos
  from sympy.external import import_module
  from sympy.logic.algorithms.lra_theory import LRASolver, UnhandledInput, LRARational, HANDLE_NEGATION
  from sympy.core.random import random, choice, randint
  from sympy.core.sympify import sympify
  from sympy.ntheory.generate import randprime
  from sympy.core.relational import StrictLessThan, StrictGreaterThan
  import itertools
  from sympy.testing.pytest import raises, XFAIL, skip
label_desc: Use image node_id 7 for calling a global function with example usage: test_random_problems() without return types