diff --git a/src/nagini_contracts/contracts.py b/src/nagini_contracts/contracts.py
index 2a1aa1b0..ee2ebe07 100644
--- a/src/nagini_contracts/contracts.py
+++ b/src/nagini_contracts/contracts.py
@@ -433,7 +433,7 @@ def ToMS(s: PSeq[T]) -> PMultiset[T]:
 # The following annotations have no runtime semantics. They are only used for
 # the Python to Viper translation.
 
-def Acc(field, ratio=1) -> bool:
+def Acc(field, ratio: float=1) -> bool:
     """
     Access permission to field.
     0 < ratio < 1 means read-only access.
diff --git a/src/nagini_translation/conftest.py b/src/nagini_translation/conftest.py
index 183d4d03..c9776519 100644
--- a/src/nagini_translation/conftest.py
+++ b/src/nagini_translation/conftest.py
@@ -42,6 +42,7 @@
 _IO_TESTS_DIR = 'tests/io/'
 _OBLIGATIONS_TESTS_DIR = 'tests/obligations/'
 _ARP_TESTS_DIR = 'tests/arp/'
+_STRICT_INT_TESTS_DIR = 'tests/strict-int/'
 
 
 class PyTestConfig:
@@ -86,6 +87,8 @@ def add_test(self, test: str):
             self._add_test_dir(_OBLIGATIONS_TESTS_DIR)
         elif test == 'arp':
             self._add_test_dir(_ARP_TESTS_DIR)
+        elif test == 'strict-int':
+            self._add_test_dir(_STRICT_INT_TESTS_DIR)
         elif test == _TRANSLATION_TESTS_SUFFIX:
             self._add_test_mode(_TRANSLATION_TESTS_SUFFIX)
         elif test == _VERIFICATION_TESTS_SUFFIX:
@@ -160,6 +163,7 @@ def pytest_addoption(parser: 'pytest.config.Parser'):
     parser.addoption('--io', dest='io', action='store_true')
     parser.addoption('--obligations', dest='obligations', action='store_true')
     parser.addoption('--arp', dest='arp', action='store_true')
+    parser.addoption('--strict-int-tests', dest='strict_int_tests', action='store_true')
     parser.addoption('--all-verifiers', dest='all_verifiers',
                      action='store_true')
     parser.addoption('--silicon', dest='silicon', action='store_true')
@@ -177,7 +181,7 @@ def pytest_configure(config: 'pytest.config.Config'):
     # Setup tests.
     tests = []
     if config.option.all_tests:
-        tests = ['functional', 'sif-true', 'sif-poss', 'sif-prob', 'io', 'obligations', 'arp']
+        tests = ['functional', 'sif-true', 'sif-poss', 'sif-prob', 'io', 'obligations', 'arp', 'strict-int']
     else:
         if config.option.functional:
             tests.append('functional')
@@ -195,6 +199,8 @@ def pytest_configure(config: 'pytest.config.Config'):
             tests.append('obligations')
         if config.option.arp:
             tests.append('arp')
+        if config.option.strict_int_tests:
+            tests.append('strict-int')
         if config.option.translation:
             tests.append('translation')
         if config.option.verification:
@@ -293,9 +299,10 @@ def pytest_generate_tests(metafunc: 'pytest.python.Metafunc'):
                     sif = False
                 reload_resources = file in reload_triggers
                 arp = 'arp' in file
+                strict_int = 'strict-int' in file
                 base = file.partition('translation')[0] + 'translation'
-                params.append((file, base, sif, reload_resources, arp, float_encoding))
-        metafunc.parametrize('path,base,sif,reload_resources,arp,float_encoding', params)
+                params.append((file, base, sif, reload_resources, arp, strict_int, float_encoding))
+        metafunc.parametrize('path,base,sif,reload_resources,arp,strict_int,float_encoding', params)
     elif func_name == _VERIFICATION_TEST_FUNCTION_NAME:
         if not _pytest_config.selected_modes or 'verification' in _pytest_config.selected_modes:
             for test_dir in _pytest_config.verification_test_dirs:
@@ -331,12 +338,13 @@ def pytest_generate_tests(metafunc: 'pytest.python.Metafunc'):
                 reload_resources = (file in reload_triggers) or (new_float_encoding != float_encoding)
                 float_encoding = new_float_encoding
                 arp = 'arp' in file
+                strict_int = 'strict-int' in file
                 base = file.partition('verification')[0] + 'verification'
                 params.extend([(file, base, verifier, sif, reload_resources, arp,
                                 ignore_obligations or (None if verifier == 'silicon' else False),
-                                _pytest_config.store_viper, float_encoding, select) for verifier
+                                _pytest_config.store_viper, float_encoding, select, strict_int) for verifier
                                in _pytest_config.verifiers])
-        metafunc.parametrize('path,base,verifier,sif,reload_resources,arp,ignore_obligations,print,float_encoding,selection', params)
+        metafunc.parametrize('path,base,verifier,sif,reload_resources,arp,ignore_obligations,print,float_encoding,selection,strict_int', params)
     else:
         pytest.exit('Unrecognized test function.')
 
diff --git a/src/nagini_translation/lib/context.py b/src/nagini_translation/lib/context.py
index 21f859e4..69eb287c 100644
--- a/src/nagini_translation/lib/context.py
+++ b/src/nagini_translation/lib/context.py
@@ -64,6 +64,7 @@ def __init__(self) -> None:
         self.sif = False
         self.allow_statements = False
         self.float_encoding = None
+        self.strict_int = False
 
     def get_fresh_int(self) -> int:
         """
diff --git a/src/nagini_translation/main.py b/src/nagini_translation/main.py
index e9827bea..9a264e44 100755
--- a/src/nagini_translation/main.py
+++ b/src/nagini_translation/main.py
@@ -111,7 +111,7 @@ def translate(path: str, jvm: JVM, bv_size: int, selected: Set[str] = set(), bas
               sif: bool = False, arp: bool = False, ignore_global: bool = False,
               reload_resources: bool = False, verbose: bool = False,
               check_consistency: bool = False, float_encoding: str = None,
-              counterexample: bool = False) -> Tuple[List['PythonModule'], Program]:
+              counterexample: bool = False, strict_int: bool = False) -> Tuple[List['PythonModule'], Program]:
     """
     Translates the Python module at the given path to a Viper program
     """
@@ -154,7 +154,8 @@ def translate(path: str, jvm: JVM, bv_size: int, selected: Set[str] = set(), bas
         sil_programs = load_sil_files(jvm, bv_size, sif, float_encoding)
     modules = [main_module.global_module] + list(analyzer.modules.values())
     prog = translator.translate_program(modules, sil_programs, selected,
-                                        arp=arp, ignore_global=ignore_global, sif=sif, float_encoding=float_encoding)
+                                        arp=arp, ignore_global=ignore_global, sif=sif, float_encoding=float_encoding,
+                                        strict_int=strict_int)
     if sif:
         set_all_low_methods(jvm, viper_ast.all_low_methods)
         set_preserves_low_methods(jvm, viper_ast.preserves_low_methods)
@@ -384,6 +385,12 @@ def main() -> None:
         type=int,
         default=8
     )
+    parser.add_argument(
+        '--strict-int',
+        action='store_true',
+        default=False,
+        help='Require exact int type (type(x) == int) rather than subtype (isinstance(x, int)) in many places.'
+    )
     parser.add_argument(
         '--disable-branch-conditions',
         help='Disable reporting of branch conditions for verification errors with the Silicon backend..',
@@ -506,7 +513,8 @@ def translate_and_verify(python_file, jvm, args, print=print, arp=False, base_di
             selected = set(args.select.split(',')) if args.select else set()
         modules, prog = translate(python_file, jvm, args.int_bitops_size, selected=selected, sif=args.sif, base_dir=base_dir,
                                   ignore_global=args.ignore_global, arp=arp, verbose=args.verbose,
-                                  counterexample=args.counterexample, float_encoding=args.float_encoding)
+                                  counterexample=args.counterexample, float_encoding=args.float_encoding,
+                                  strict_int=args.strict_int)
         if args.print_viper:
             if args.verbose:
                 print('Result:')
@@ -526,7 +534,8 @@ def translate_and_verify(python_file, jvm, args, print=print, arp=False, base_di
             for i in range(args.benchmark):
                 start = time.time()
                 modules, prog = translate(python_file, jvm, args.int_bitops_size, selected=selected, sif=args.sif, arp=arp, base_dir=base_dir,
-                                          ignore_global=args.ignore_global, float_encoding=args.float_encoding)
+                                          ignore_global=args.ignore_global, float_encoding=args.float_encoding,
+                                          strict_int=args.strict_int)
                 vresult = verify(modules, prog, python_file, jvm, viper_args, backend=backend, arp=arp)
                 end = time.time()
                 print("{}, {}, {}, {}, {}".format(
@@ -540,7 +549,7 @@ def translate_and_verify(python_file, jvm, args, print=print, arp=False, base_di
             vresult = verify(modules, prog, python_file, jvm, viper_args,
                              backend=backend, arp=arp, counterexample=args.counterexample,
                              sif=args.sif, disable_branch_conditions=args.disable_branch_conditions)
-            
+
             if submitter is not None:
                 submitter.setSuccess(vresult.__bool__())
                 submitter.submit()
diff --git a/src/nagini_translation/mcp_server.py b/src/nagini_translation/mcp_server.py
index f5b14639..887f3fed 100644
--- a/src/nagini_translation/mcp_server.py
+++ b/src/nagini_translation/mcp_server.py
@@ -136,7 +136,7 @@ def configure(options: dict) -> dict:
 
     Recognized keys: `verifier` ('silicon' or 'carbon'), `z3Path`, `boogiePath`,
     `mypyPath`, `sif`, `intBitopsSize`, `floatEncoding`, `useViperServer`,
-    `disableBranchConditions`. `viperJarPath` cannot be changed after startup and
+    `disableBranchConditions`, `strictInt`. `viperJarPath` cannot be changed after startup and
     is ignored. Unknown or null keys are ignored. Changing
     `sif`/`intBitopsSize`/`floatEncoding` reloads the Silver resources;
     already-running verifications are unaffected.
diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil
index bd4737b3..52daf5c1 100644
--- a/src/nagini_translation/resources/bool.sil
+++ b/src/nagini_translation/resources/bool.sil
@@ -325,6 +325,7 @@ function int___eq__(self: Ref, other: Ref): Bool
     ensures issubtype(typeof(other), int()) ==> result == int___unbox__(self) == int___unbox__(other)
     ensures issubtype(typeof(other), int()) ==> result == object___eq__(self, other)
     ensures issubtype(typeof(other), float()) ==> result == float___eq__(self, other)
+    ensures result == object___eq__(self, other)
 
 
 function bool___eq__(self: Ref, other: Ref): Bool
diff --git a/src/nagini_translation/resources/list.sil b/src/nagini_translation/resources/list.sil
index 063d550a..5f61f054 100644
--- a/src/nagini_translation/resources/list.sil
+++ b/src/nagini_translation/resources/list.sil
@@ -20,7 +20,8 @@ function list___contains__(self: Ref, item: Ref): Bool
     decreases _
     requires issubtype(typeof(self), list(list_arg(typeof(self), 0)))
     requires acc(self.list_acc, wildcard)
-    ensures result == (item in self.list_acc)
+    ensures result == exists i: Ref :: object___eq__(item, i) && i in self.list_acc
+    ensures item in self.list_acc ==> result
 
 function list___bool__(self: Ref) : Bool
     decreases _
diff --git a/src/nagini_translation/resources/seq.sil b/src/nagini_translation/resources/seq.sil
index f494849b..91a08ebf 100644
--- a/src/nagini_translation/resources/seq.sil
+++ b/src/nagini_translation/resources/seq.sil
@@ -17,7 +17,8 @@ function PSeq___sil_seq__(box: Ref): Seq[Ref]
 function PSeq___contains__(self: Ref, item: Ref): Bool
     decreases _
     requires issubtype(typeof(self), PSeq(PSeq_arg(typeof(self), 0)))
-    ensures result == (item in PSeq___sil_seq__(self))
+    ensures result == exists i: Ref :: object___eq__(item, i) && i in PSeq___sil_seq__(self)
+    ensures item in PSeq___sil_seq__(self) ==> result
     ensures result ==> issubtype(typeof(item), PSeq_arg(typeof(self), 0))
 
 function PSeq___getitem__(self: Ref, index: Ref): Ref
diff --git a/src/nagini_translation/service.py b/src/nagini_translation/service.py
index cbafa6e0..ffd469be 100644
--- a/src/nagini_translation/service.py
+++ b/src/nagini_translation/service.py
@@ -127,7 +127,9 @@ def __init__(self, *, z3_path: str = None, viper_jar_path: str = None,
                  int_bitops_size: int = 8, use_viper_server: bool = True,
                  verifier_backend: str = 'silicon', sif=False,
                  float_encoding: str = None,
-                 disable_branch_conditions: bool = False):
+                 disable_branch_conditions: bool = False,
+                 strict_int: bool = False,
+                 force_obligations: bool = False):
         if viper_jar_path:
             config.classpath = viper_jar_path
         if z3_path:
@@ -151,6 +153,10 @@ def __init__(self, *, z3_path: str = None, viper_jar_path: str = None,
         self._float_encoding = float_encoding
         self._bv_size = int_bitops_size
         self._disable_branch_conditions = disable_branch_conditions
+        self._strict_int = strict_int
+        if force_obligations:
+            # False instead of None: force the obligation encoding (see main.py).
+            config.obligation_config.disable_all = False
         # The obligation encoding is auto-detected per program by translate(),
         # which persistently sets obligation_config.disable_all once a program
         # without obligations is seen. In a long-lived service that would then
@@ -280,6 +286,7 @@ def current_options(self) -> dict:
             'floatEncoding': self._float_encoding,
             'useViperServer': config.use_viper_server,
             'disableBranchConditions': self._disable_branch_conditions,
+            'strictInt': self._strict_int,
             'z3Path': config.z3_path,
             'boogiePath': config.boogie_path,
             'mypyPath': config.mypy_path,
@@ -313,6 +320,8 @@ def reconfigure(self, **options) -> dict:
             if options.get('disable_branch_conditions') is not None:
                 self._disable_branch_conditions = bool(
                     options['disable_branch_conditions'])
+            if options.get('strict_int') is not None:
+                self._strict_int = bool(options['strict_int'])
             reload_needed = False
             if options.get('sif') is not None and options['sif'] != self._sif:
                 self._sif = options['sif']
@@ -349,7 +358,8 @@ def _verify_concurrent(self, path, selected, base_dir, counterexample,
                     path, self.jvm, self._bv_size,
                     selected=set(selected) if selected else set(), sif=False,
                     base_dir=base_dir, arp=False, counterexample=counterexample,
-                    ignore_global=ignore_global, float_encoding=self._float_encoding)
+                    ignore_global=ignore_global, float_encoding=self._float_encoding,
+                    strict_int=self._strict_int)
             except (TypeException, InvalidProgramException, UnsupportedException) as e:
                 return VerifyResult(False, self._exception_diagnostics(e, path),
                                     time.time() - start, translation_failed=True)
@@ -427,7 +437,8 @@ def _verify_serial(self, path, selected, base_dir, arp,
                 path, self.jvm, self._bv_size, selected=selected_set,
                 sif=self._sif, base_dir=base_dir, arp=arp,
                 counterexample=counterexample, ignore_global=ignore_global,
-                float_encoding=self._float_encoding)
+                float_encoding=self._float_encoding,
+                strict_int=self._strict_int)
             if translated is None:
                 return VerifyResult(False, [self._point_diagnostic(
                     path, 'Type checking failed.', 'type.error')],
@@ -550,6 +561,7 @@ def _point_diagnostic(path: str, message: str, code: str) -> Diagnostic:
     'floatEncoding': 'float_encoding',
     'useViperServer': 'use_viper_server',
     'disableBranchConditions': 'disable_branch_conditions',
+    'strictInt': 'strict_int',
 }
 
 
@@ -586,6 +598,12 @@ def add_service_arguments(parser: argparse.ArgumentParser) -> argparse.ArgumentP
                              'errors (Silicon backend)')
     parser.add_argument('--no-viper-server', action='store_true',
                         help='disable the in-process ViperServer backend')
+    parser.add_argument('--strict-int', action='store_true', default=False,
+                        help='require exact int type (type(x) == int) rather '
+                             'than subtype (isinstance(x, int)) in many places')
+    parser.add_argument('--force-obligations', action='store_true', default=False,
+                        help='force use of the obligations encoding used to '
+                             'verify liveness properties')
     return parser
 
 
@@ -601,7 +619,8 @@ def service_kwargs_from_args(args: argparse.Namespace) -> dict:
         mypy_path=args.mypy_path, int_bitops_size=args.int_bitops_size,
         use_viper_server=not args.no_viper_server, verifier_backend=args.verifier,
         sif=args.sif, float_encoding=args.float_encoding,
-        disable_branch_conditions=args.disable_branch_conditions)
+        disable_branch_conditions=args.disable_branch_conditions,
+        strict_int=args.strict_int, force_obligations=args.force_obligations)
 
 
 def make_service(args: argparse.Namespace) -> VerificationService:
diff --git a/src/nagini_translation/tests.py b/src/nagini_translation/tests.py
index 50870be4..3f0f42b9 100644
--- a/src/nagini_translation/tests.py
+++ b/src/nagini_translation/tests.py
@@ -582,7 +582,7 @@ class VerificationTest(AnnotatedTest):
     def test_file(
             self, path: str, base: str, jvm: jvmaccess.JVM, verifier: ViperVerifier,
             sif: bool, reload_resources: bool, arp: bool, ignore_obligations: bool, store_viper: bool,
-            float_encoding: Optional[str], selection: Set[str]):
+            float_encoding: Optional[str], selection: Set[str], strict_int: bool = False):
         """Test specific Python file."""
         config.obligation_config.disable_all = ignore_obligations
         annotation_manager = self.get_annotation_manager(path, verifier.name)
@@ -593,7 +593,7 @@ def test_file(
         abspath = os.path.abspath(path)
         absbase = os.path.abspath(base)
         modules, prog = translate(abspath, jvm, 8, base_dir=absbase, sif=sif, arp=arp, reload_resources=reload_resources,
-                                  float_encoding=float_encoding, selected=selection)
+                                  float_encoding=float_encoding, selected=selection, strict_int=strict_int)
         assert prog is not None
         if store_viper:
             import string
@@ -643,17 +643,18 @@ def _evaluate_result(
 _VERIFICATION_TESTER = VerificationTest()
 
 
-def test_verification(path, base, verifier, sif, reload_resources, arp, ignore_obligations, print, float_encoding, selection):
+def test_verification(path, base, verifier, sif, reload_resources, arp, ignore_obligations, print, float_encoding, selection, strict_int):
     """Execute provided verification test."""
     _VERIFICATION_TESTER.test_file(path, base, _JVM, verifier, sif, reload_resources, arp, ignore_obligations,
-                                   print, float_encoding, selection)
+                                   print, float_encoding, selection, strict_int)
 
 
 class TranslationTest(AnnotatedTest):
     """Test for testing translation errors."""
 
     def test_file(self, path: str, base: str, jvm: jvmaccess.JVM, sif: bool,
-                  reload_resources: bool, arp: bool, float_encoding: Optional[str]):
+                  reload_resources: bool, arp: bool, float_encoding: Optional[str],
+                  strict_int: bool = False):
         """Test specific Python file."""
         annotation_manager = self.get_annotation_manager(path, _BACKEND_ANY)
         if annotation_manager.ignore_file():
@@ -662,7 +663,7 @@ def test_file(self, path: str, base: str, jvm: jvmaccess.JVM, sif: bool,
         base = os.path.abspath(base)
         try:
             translate(path, jvm, 8, base_dir=base, sif=sif, arp=arp, reload_resources=reload_resources,
-                      float_encoding=float_encoding)
+                      float_encoding=float_encoding, strict_int=strict_int)
             actual_errors = []
         except InvalidProgramException as exp1:
             actual_errors = [InvalidProgramError(exp1)]
@@ -680,6 +681,6 @@ def test_file(self, path: str, base: str, jvm: jvmaccess.JVM, sif: bool,
 _TRANSLATION_TESTER = TranslationTest()
 
 
-def test_translation(path, base, sif, reload_resources, arp, float_encoding):
+def test_translation(path, base, sif, reload_resources, arp, strict_int, float_encoding):
     """Execute provided translation test."""
-    _TRANSLATION_TESTER.test_file(path, base, _JVM, sif, reload_resources, arp, float_encoding)
+    _TRANSLATION_TESTER.test_file(path, base, _JVM, sif, reload_resources, arp, float_encoding, strict_int)
diff --git a/src/nagini_translation/translator.py b/src/nagini_translation/translator.py
index 8950df90..e10215fd 100644
--- a/src/nagini_translation/translator.py
+++ b/src/nagini_translation/translator.py
@@ -91,7 +91,8 @@ def translate_program(self, modules: List[PythonModule], sil_progs: List,
                           ignore_global: bool = False,
                           arp: bool = False,
                           float_encoding : str = None,
-                          sif = False) -> 'silver.ast.Program':
+                          sif = False,
+                          strict_int: bool = False) -> 'silver.ast.Program':
         ctx = Context()
         ctx.sif = sif
         ctx.current_class = None
@@ -99,6 +100,7 @@ def translate_program(self, modules: List[PythonModule], sil_progs: List,
         ctx.module = modules[0]
         ctx.arp = arp
         ctx.float_encoding = float_encoding
+        ctx.strict_int = strict_int
         return self.prog_translator.translate_program(modules, sil_progs, ctx,
                                                       selected, ignore_global)
 
diff --git a/src/nagini_translation/translators/contract.py b/src/nagini_translation/translators/contract.py
index 7559da18..715fb4f7 100644
--- a/src/nagini_translation/translators/contract.py
+++ b/src/nagini_translation/translators/contract.py
@@ -144,7 +144,13 @@ def translate_builtin_predicate(self, node: ast.Call, perm: Expr,
         pos = self.to_position(node, ctx)
         if name == 'list_pred':
             # field list_acc : Seq[Ref]
-            return self._get_field_perm('list_acc', seq_ref, perm, args[0], pos, ctx)
+            field_perm = self._get_field_perm('list_acc', seq_ref, perm,
+                                              args[0], pos, ctx)
+            strict_inv = self._strict_int_list_invariant(node.args[0], args[0],
+                                                         pos, ctx)
+            if strict_inv is None:
+                return field_perm
+            return self.viper.And(field_perm, strict_inv, pos, self.no_info(ctx))
         elif name == 'set_pred':
             # field set_acc : Set[Ref]
             return self._get_field_perm('set_acc', set_ref, perm, args[0], pos, ctx)
@@ -169,6 +175,40 @@ def _get_field_perm(self, field_name: str, field_type: 'silver.ast.Type', perm:
         pred = self.viper.FieldAccessPredicate(field_acc, perm, pos, info)
         return pred
 
+    def _strict_int_list_invariant(self, list_py_node: ast.AST, list_ref: Expr,
+                                   pos: Position, ctx: Context) -> Expr:
+        # In strict-int mode, List[int] elements must be exactly int (not bool
+        # or any other int subtype). Returns a quantified invariant:
+        #     forall i :: 0 <= i < |l.list_acc| ==> typeof(l.list_acc[i]) == int()
+        # or None when the invariant doesn't apply.
+        if not ctx.strict_int:
+            return None
+        list_type = self.get_type(list_py_node, ctx)
+        if list_type is None or not getattr(list_type, 'type_args', None):
+            return None
+        if list_type.type_args[0].name != INT_TYPE:
+            return None
+        info = self.no_info(ctx)
+        seq_ref = self.viper.SeqType(self.viper.Ref)
+        field = self.viper.Field('list_acc', seq_ref, pos, info)
+        field_acc = self.viper.FieldAccess(list_ref, field, pos, info)
+        i_decl = self.viper.LocalVarDecl('i', self.viper.Int, pos, info)
+        i_ref = self.viper.LocalVar('i', self.viper.Int, pos, info)
+        seq_at_i = self.viper.SeqIndex(field_acc, i_ref, pos, info)
+        zero = self.viper.IntLit(0, pos, info)
+        length = self.viper.SeqLength(field_acc, pos, info)
+        bounds = self.viper.And(
+            self.viper.LeCmp(zero, i_ref, pos, info),
+            self.viper.LtCmp(i_ref, length, pos, info),
+            pos, info)
+        int_cls = ctx.module.global_module.classes[INT_TYPE]
+        int_lit = self.type_factory.translate_type_literal(int_cls, pos, ctx)
+        typeof_at_i = self.type_factory.typeof(seq_at_i, ctx)
+        eq = self.viper.EqCmp(typeof_at_i, int_lit, pos, info)
+        body = self.viper.Implies(bounds, eq, pos, info)
+        trigger = self.viper.Trigger([seq_at_i], pos, info)
+        return self.viper.Forall([i_decl], [trigger], body, pos, info)
+
     def translate_may_start(self, node: ast.Call, args: List[Expr], perm: Expr,
                             ctx: Context) -> Expr:
         pos = self.to_position(node, ctx)
diff --git a/src/nagini_translation/translators/statement.py b/src/nagini_translation/translators/statement.py
index 79d1beac..f75e1195 100644
--- a/src/nagini_translation/translators/statement.py
+++ b/src/nagini_translation/translators/statement.py
@@ -608,6 +608,27 @@ def _create_for_loop_invariant(self, iter_var: PythonVar, seq_temp_var: PythonVa
         invariant.append(self.viper.Implies(some_error, previous_is_all, pos,
                                             info))
         invariant.append(self.viper.Implies(empty_iterator, some_error, pos, info))
+
+        if ctx.strict_int and target_var.type.name == INT_TYPE:
+            # Carry the strict element-type fact across the loop body. Without
+            # this, __next__'s `issubtype(typeof(_res), int())` postcondition
+            # cannot establish the strict `typeof(target) == int()` that the
+            # target_type invariant above requires in strict-int mode.
+            i_decl = self.viper.LocalVarDecl('__si_i', self.viper.Int, pos, info)
+            i_ref = self.viper.LocalVar('__si_i', self.viper.Int, pos, info)
+            seq_at_i = self.viper.SeqIndex(iter_acc, i_ref, pos, info)
+            bounds = self.viper.And(
+                self.viper.LeCmp(zero, i_ref, pos, info),
+                self.viper.LtCmp(i_ref, iter_list_len, pos, info),
+                pos, info)
+            int_cls = ctx.module.global_module.classes[INT_TYPE]
+            int_lit = self.type_factory.translate_type_literal(int_cls, pos, ctx)
+            typeof_eq = self.viper.EqCmp(self.type_factory.typeof(seq_at_i, ctx),
+                                         int_lit, pos, info)
+            forall_body = self.viper.Implies(bounds, typeof_eq, pos, info)
+            trigger = self.viper.Trigger([seq_at_i], pos, info)
+            invariant.append(self.viper.Forall([i_decl], [trigger], forall_body,
+                                               pos, info))
         return invariant
 
     def _get_iterator(self, iterable: Expr, iterable_type: PythonType,
diff --git a/src/nagini_translation/translators/type.py b/src/nagini_translation/translators/type.py
index 4552593b..26789464 100644
--- a/src/nagini_translation/translators/type.py
+++ b/src/nagini_translation/translators/type.py
@@ -9,7 +9,10 @@
 
 from nagini_translation.lib.constants import (
     CALLABLE_TYPE,
+    INT_TYPE,
     PRIMITIVES,
+    PSEQ_TYPE,
+    TUPLE_TYPE,
 )
 from nagini_translation.lib.program_nodes import (
     PythonClass,
@@ -100,4 +103,117 @@ def type_check(self, lhs: Expr, type: PythonType,
             return self.viper.TrueLit(position, self.no_info(ctx))
         else:
             result = self.type_factory.type_check(lhs, type, position, ctx)
+            strict_inv = self._strict_int_pseq_invariant(lhs, type, position, ctx)
+            if strict_inv is not None:
+                result = self.viper.And(result, strict_inv, position,
+                                        self.no_info(ctx))
+            tuple_inv = self._strict_int_tuple_invariant(lhs, type, position, ctx)
+            if tuple_inv is not None:
+                result = self.viper.And(result, tuple_inv, position,
+                                        self.no_info(ctx))
             return result
+
+    def _strict_int_pseq_invariant(self, pseq_ref: Expr, pseq_type: PythonType,
+                                   pos: 'silver.ast.Position',
+                                   ctx: Context) -> Optional[Expr]:
+        # Mirror of _strict_int_list_invariant for PSeq[int]: in strict-int
+        # mode, every element of a PSeq[int] must have exactly type int. Since
+        # PSeq is a value type with no permission to attach the invariant to,
+        # we conjoin it with the type check that establishes
+        # `typeof(s) == PSeq(int())`. Returns None when not applicable.
+        if not ctx.strict_int:
+            return None
+        if pseq_type is None or pseq_type.name != PSEQ_TYPE:
+            return None
+        if not getattr(pseq_type, 'type_args', None):
+            return None
+        if pseq_type.type_args[0].name != INT_TYPE:
+            return None
+        info = self.no_info(ctx)
+        seq_class = ctx.module.global_module.classes[PSEQ_TYPE]
+        sil_seq = self.get_function_call(seq_class, '__sil_seq__',
+                                         [pseq_ref], [None], None, ctx, pos)
+        i_decl = self.viper.LocalVarDecl('i', self.viper.Int, pos, info)
+        i_ref = self.viper.LocalVar('i', self.viper.Int, pos, info)
+        seq_at_i = self.viper.SeqIndex(sil_seq, i_ref, pos, info)
+        zero = self.viper.IntLit(0, pos, info)
+        length = self.viper.SeqLength(sil_seq, pos, info)
+        bounds = self.viper.And(
+            self.viper.LeCmp(zero, i_ref, pos, info),
+            self.viper.LtCmp(i_ref, length, pos, info),
+            pos, info)
+        int_cls = ctx.module.global_module.classes[INT_TYPE]
+        int_lit = self.type_factory.translate_type_literal(int_cls, pos, ctx)
+        typeof_at_i = self.type_factory.typeof(seq_at_i, ctx)
+        eq = self.viper.EqCmp(typeof_at_i, int_lit, pos, info)
+        body = self.viper.Implies(bounds, eq, pos, info)
+        trigger = self.viper.Trigger([seq_at_i], pos, info)
+        return self.viper.Forall([i_decl], [trigger], body, pos, info)
+
+    def _strict_int_tuple_invariant(self, tuple_ref: Expr,
+                                    tuple_type: PythonType,
+                                    pos: 'silver.ast.Position',
+                                    ctx: Context) -> Optional[Expr]:
+        # In strict-int mode, tuple element access only guarantees a subtype
+        # of the slot type because `tuple___getitem__` ensures
+        # `issubtype(typeof(result), tuple_arg(typeof(self), key))`. For int
+        # slots we need exact equality. Anchor on `tuple___sil_seq__(t)` (which
+        # carries `|result| == tuple___len__(self)` for in-bounds SeqIndex) and
+        # also offer `tuple___val__(t)[i]` as an alternate trigger so the
+        # quantifier fires on the term `tuple___getitem__`'s ensures puts in
+        # scope at the call site.
+        if not ctx.strict_int:
+            return None
+        if tuple_type is None or tuple_type.name != TUPLE_TYPE:
+            return None
+        type_args = getattr(tuple_type, 'type_args', None)
+        if not type_args:
+            return None
+        info = self.no_info(ctx)
+        tuple_class = ctx.module.global_module.classes[TUPLE_TYPE]
+        sil_seq = self.get_function_call(tuple_class, '__sil_seq__',
+                                         [tuple_ref], [None], None, ctx, pos)
+        seq_ref_type = self.viper.SeqType(self.viper.Ref)
+        tuple_val = self.viper.FuncApp('tuple___val__', [tuple_ref], pos, info,
+                                       seq_ref_type)
+        int_cls = ctx.module.global_module.classes[INT_TYPE]
+        int_lit = self.type_factory.translate_type_literal(int_cls, pos, ctx)
+        if getattr(tuple_type, 'exact_length', True):
+            # Heterogeneous tuple: emit a conjunct per int slot. Indexing into
+            # `tuple___sil_seq__` carries the length axiom so in-bounds checks
+            # succeed for known slot indices.
+            conjuncts = []
+            for i, arg_type in enumerate(type_args):
+                if arg_type is None or arg_type.name != INT_TYPE:
+                    continue
+                idx = self.viper.IntLit(i, pos, info)
+                at_i = self.viper.SeqIndex(sil_seq, idx, pos, info)
+                typeof_at_i = self.type_factory.typeof(at_i, ctx)
+                conjuncts.append(self.viper.EqCmp(typeof_at_i, int_lit, pos,
+                                                  info))
+            if not conjuncts:
+                return None
+            result = conjuncts[0]
+            for c in conjuncts[1:]:
+                result = self.viper.And(result, c, pos, info)
+            return result
+        # Variadic Tuple[T, ...]: single element type.
+        if type_args[0] is None or type_args[0].name != INT_TYPE:
+            return None
+        i_decl = self.viper.LocalVarDecl('i', self.viper.Int, pos, info)
+        i_ref = self.viper.LocalVar('i', self.viper.Int, pos, info)
+        sil_at_i = self.viper.SeqIndex(sil_seq, i_ref, pos, info)
+        val_at_i = self.viper.SeqIndex(tuple_val, i_ref, pos, info)
+        zero = self.viper.IntLit(0, pos, info)
+        length = self.viper.SeqLength(sil_seq, pos, info)
+        bounds = self.viper.And(
+            self.viper.LeCmp(zero, i_ref, pos, info),
+            self.viper.LtCmp(i_ref, length, pos, info),
+            pos, info)
+        typeof_at_i = self.type_factory.typeof(sil_at_i, ctx)
+        eq = self.viper.EqCmp(typeof_at_i, int_lit, pos, info)
+        body = self.viper.Implies(bounds, eq, pos, info)
+        trig_sil = self.viper.Trigger([sil_at_i], pos, info)
+        trig_val = self.viper.Trigger([val_at_i], pos, info)
+        return self.viper.Forall([i_decl], [trig_sil, trig_val], body, pos,
+                                 info)
diff --git a/src/nagini_translation/translators/type_domain_factory.py b/src/nagini_translation/translators/type_domain_factory.py
index 1f0fc8c9..b03205a1 100644
--- a/src/nagini_translation/translators/type_domain_factory.py
+++ b/src/nagini_translation/translators/type_domain_factory.py
@@ -819,6 +819,10 @@ def type_check(self, lhs: 'Expr', type: 'PythonType',
         is a subtype of (or, if ``concrete`` is true, equivalent to) the given
         ``type``.
         """
+        if (ctx.strict_int
+                and isinstance(type, PythonClass)
+                and type.name == 'int'):
+            concrete = True
         info = self.no_info(ctx)
         type_func = self.typeof(lhs, ctx)
         if isinstance(type, OptionalType):
diff --git a/tests/servers/test_verification_options.py b/tests/servers/test_verification_options.py
index e6b2a39a..475334e4 100644
--- a/tests/servers/test_verification_options.py
+++ b/tests/servers/test_verification_options.py
@@ -150,3 +150,26 @@ def test_include_viper_returns_translated_program(service, tmp_path):
     default = service.verify(_write(tmp_path, "iv2.py", _NO_OBLIGATIONS_SRC))
     assert default.viper_program is None
     assert "viperProgram" not in default.to_dict()
+
+
+# -- strictInt --------------------------------------------------------------
+
+_BOOL_AS_INT_SRC = (
+    "from nagini_contracts.contracts import *\n\n"
+    "def f() -> int:\n"
+    "    return True\n"
+)
+
+
+def test_strict_int_toggles_bool_int_conformance(service, tmp_path):
+    path = _write(tmp_path, "strict_int.py", _BOOL_AS_INT_SRC)
+    # Off by default: bool is a subtype of int.
+    assert service.verify(path).success
+    service.reconfigure(strict_int=True)
+    try:
+        strict = service.verify(path)
+        assert not strict.success
+        assert any("postcondition" in d.code for d in strict.diagnostics)
+    finally:
+        service.reconfigure(strict_int=False)
+    assert service.verify(path).success
diff --git a/tests/strict-int/verification/test_strict_int.py b/tests/strict-int/verification/test_strict_int.py
new file mode 100644
index 00000000..87e76c48
--- /dev/null
+++ b/tests/strict-int/verification/test_strict_int.py
@@ -0,0 +1,134 @@
+"""
+Copyright (c) 2019 ETH Zurich
+This Source Code Form is subject to the terms of the Mozilla Public
+License, v. 2.0. If a copy of the MPL was not distributed with this
+file, You can obtain one at http://mozilla.org/MPL/2.0/.
+"""
+from nagini_contracts.contracts import *
+from typing import List, Tuple
+
+
+def takes_int(x: int) -> None:
+    Requires(True)
+
+
+def test_int_arg_accepted() -> None:
+    takes_int(42)
+
+
+def test_bool_arg_rejected() -> None:
+    #:: ExpectedOutput(call.precondition:assertion.false)
+    takes_int(True)
+
+
+#:: ExpectedOutput(postcondition.violated:assertion.false)
+def returns_bool_as_int() -> int:
+    return True
+
+
+def test_forall_int_verifies() -> None:
+    Assert(Forall(int, lambda k: (k is not True and k is not False, [])))
+
+
+def sum_int_list(lst: List[int]) -> int:
+    Requires(Acc(list_pred(lst), 1 / 2))
+    Ensures(Acc(list_pred(lst), 1 / 2))
+    total = 0
+    for x in lst:
+        Invariant(Acc(list_pred(lst), 1 / 4))
+        takes_int(x)
+        total = total + x
+    return total
+
+
+def test_append_int_accepted() -> None:
+    lst = [1, 2, 3]
+    lst.append(4)
+    assert lst[3] == 4
+
+
+def append_bool_breaks_list_pred(lst: List[int]) -> None:
+    # Appending a bool to a List[int] verifies (list_append only requires
+    # issubtype), but the bool then poisons the element-type invariant, so
+    # list_pred cannot be re-established at the postcondition.
+    Requires(Acc(list_pred(lst)))
+    #:: ExpectedOutput(postcondition.violated:assertion.false)
+    Ensures(Acc(list_pred(lst)))
+    lst.append(True)
+
+
+def reads_pseq_int_param(s: PSeq[int]) -> None:
+    Requires(len(s) > 0)
+    takes_int(s[0])
+
+
+def reads_pseq_via_toseq(lst: List[int]) -> None:
+    Requires(Acc(list_pred(lst)))
+    Requires(len(lst) > 0)
+    Ensures(Acc(list_pred(lst)))
+    s = ToSeq(lst)
+    takes_int(s[0])
+
+
+def reads_pseq_int_literal() -> None:
+    s = PSeq(1, 2, 3)
+    takes_int(s[0])
+
+
+def reads_pseq_bool_param_rejected(s: PSeq[bool]) -> None:
+    # PSeq[bool] elements must NOT be promoted to strict int.
+    Requires(len(s) > 0)
+    #:: ExpectedOutput(call.precondition:assertion.false)
+    takes_int(s[0])
+
+
+def reads_tuple_int_param(t: Tuple[int, int]) -> None:
+    takes_int(t[0])
+    takes_int(t[1])
+
+
+def reads_single_int_tuple(t: Tuple[int]) -> None:
+    takes_int(t[0])
+
+
+def reads_homogeneous_tuple(t: Tuple[int, ...]) -> None:
+    Requires(len(t) > 0)
+    takes_int(t[0])
+
+
+def reads_mixed_tuple(t: Tuple[int, str]) -> None:
+    # Only the int slot can be passed to takes_int.
+    takes_int(t[0])
+
+
+def tuple_literal_strict() -> None:
+    t = (1, 2, 3)
+    takes_int(t[0])
+    takes_int(t[2])
+
+
+def unpacks_tuple_int(t: Tuple[int, int]) -> None:
+    a, b = t
+    takes_int(a)
+    takes_int(b)
+
+
+def _make_int_pair() -> Tuple[int, int]:
+    return (1, 2)
+
+
+def returns_tuple_int_used() -> None:
+    t = _make_int_pair()
+    takes_int(t[0])
+
+
+def reads_bool_tuple_rejected(t: Tuple[bool, bool]) -> None:
+    # Tuple[bool, bool] elements must NOT be promoted to strict int.
+    #:: ExpectedOutput(call.precondition:assertion.false)
+    takes_int(t[0])
+
+
+def reads_bool_variadic_tuple_rejected(t: Tuple[bool, ...]) -> None:
+    Requires(len(t) > 0)
+    #:: ExpectedOutput(call.precondition:assertion.false)
+    takes_int(t[0])