new_contents: #
  # This file is part of pySMT.
  #
  #   Copyright 2014 Andrea Micheli and Marco Gario
  #
  #   Licensed under the Apache License, Version 2.0 (the "License");
  #   you may not use this file except in compliance with the License.
  #   You may obtain a copy of the License at
  #
  #       http://www.apache.org/licenses/LICENSE-2.0
  #
  #   Unless required by applicable law or agreed to in writing, software
  #   distributed under the License is distributed on an "AS IS" BASIS,
  #   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  #   See the License for the specific language governing permissions and
  #   limitations under the License.
  #
  from pysmt.shortcuts import *
  from pysmt.typing import INT, REAL, FunctionType
  from pysmt.test import TestCase, main
  from pysmt.logics import QF_UFNIA, UFNIA
  
  class TestNIA(TestCase):
  
      def test_nia_const_div_const(self):
          """Integer division between constants"""
          a = Symbol("a", INT)
          i_2 = Int(2)
          i_5 = Int(5)
  
          # a = 5/2
          check = And(Equals(a, Div(i_5, i_2)))
          for sname in get_env().factory.all_solvers(logic=QF_UFNIA):
              with Solver(name=sname) as s:
                  s.add_assertion(check)
                  c = s.solve()
                  self.assertTrue(c)
                  self.assertEqual(s.get_value(a), i_2)
  
      def test_nia_symb_div_const(self):
          """Symbol divided by constant"""
          a = Symbol("a", INT)
          i_2 = Int(2)
          i_3 = Int(3)
          i_6 = Int(6)
          i_7 = Int(7)
  
          # a > 6 & a/2 = 3
          check = And(GT(a, i_6), Equals(Div(a, i_2), i_3))
          for sname in get_env().factory.all_solvers(logic=QF_UFNIA):
              with Solver(name=sname) as s:
                  s.add_assertion(check)
                  c = s.solve()
                  self.assertTrue(c)
                  self.assertEqual(s.get_value(a), i_7)
  
      def test_nia_const_div_symb(self):
          """Constant divided by symbol"""
          a = Symbol("a", INT)
          i_0 = Int(0)
          i_2 = Int(2)
          i_5 = Int(5)
  
          # a > 0 & 5/a = 2
          check = And(GT(a, i_0), Equals(Div(i_5, a), i_2))
          for sname in get_env().factory.all_solvers(logic=QF_UFNIA):
              with Solver(name=sname) as s:
                  s.add_assertion(check)
                  c = s.solve()
                  self.assertTrue(c)
                  self.assertEqual(s.get_value(a), i_2)
  
      def test_nia_symb_div_symb(self):
          """Symbol divided by symbol"""
          a = Symbol("a", INT)
          b = Symbol("b", INT)
          i_0 = Int(0)
          i_2 = Int(2)
          i_5 = Int(5)
  
          # a = 5 & b > 0 & (a / b) = 2
          check = And(Equals(a, i_5), GT(b, i_0),
                      Equals(Div(a, b), i_2))
          for sname in get_env().factory.all_solvers(logic=QF_UFNIA):
              with Solver(name=sname) as s:
                  s.add_assertion(check)
                  c = s.solve()
                  self.assertTrue(c)
                  self.assertEqual(s.get_value(b), i_2)
  
subject: add test cases for division between integers.