code: def test_pos_neg_infinite():
      bf = (
          Q.positive_infinite(x)
          & Q.lt(x, 10000000)
          & Q.positive_infinite(y)
      )
      enc = boolean_formula_to_encoded_cnf(bf)
      lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
      for lit in enc.encoding.values():
          if lra.assert_lit(lit) is not None:
              break
      assert len(lra.enc_to_boundary) == 3
      assert lra.check()[0] == False
  
      bf = (
          Q.positive_infinite(x)
          & Q.gt(x, 10000000)
          & Q.positive_infinite(y)
      )
      enc = boolean_formula_to_encoded_cnf(bf)
      lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
      for lit in enc.encoding.values():
          if lra.assert_lit(lit) is not None:
              break
      assert len(lra.enc_to_boundary) == 3
      assert lra.check()[0] == True
  
      bf = Q.positive_infinite(x) & Q.negative_infinite(x)
      enc = boolean_formula_to_encoded_cnf(bf)
      lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
      for lit in enc.encoding.values():
          if lra.assert_lit(lit) is not None:
              break
      assert len(lra.enc_to_boundary) == 2
      assert lra.check()[0] == False
  
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 9 for calling a global function with example usage: test_pos_neg_infinite() without return types