diff --git a/src/it/scala/inox/solvers/SolvingTestSuite.scala b/src/it/scala/inox/solvers/SolvingTestSuite.scala
index 333c9d94b..4246b52a2 100644
--- a/src/it/scala/inox/solvers/SolvingTestSuite.scala
+++ b/src/it/scala/inox/solvers/SolvingTestSuite.scala
@@ -15,6 +15,7 @@ trait SolvingTestSuite extends TestSuite {
   } yield Seq(
     optSelectedSolvers(Set(solverName)),
     optCheckModels(checkModels),
+    optIgnoreModels(false),
     optAssumeChecked(assumeChecked),
     unrolling.optFeelingLucky(feelingLucky),
     unrolling.optUnrollAssumptions(unrollAssumptions),
diff --git a/src/main/scala/inox/Main.scala b/src/main/scala/inox/Main.scala
index afe269826..9acb2d11f 100644
--- a/src/main/scala/inox/Main.scala
+++ b/src/main/scala/inox/Main.scala
@@ -95,6 +95,7 @@ trait MainHelpers {
     solvers.optAssumeChecked -> Description(Solvers, "Assume that all impure expression have been checked"),
     solvers.optNoSimplifications -> Description(Solvers, "Disable selector/quantifier simplifications in solvers"),
     solvers.optCheckModels -> Description(Solvers, "Double-check counter-examples with evaluator"),
+    solvers.optIgnoreModels -> Description(Solvers, s"Do not request models from solvers.\nOverrides and disables ${optCheckModels.name} and ${unrolling.optFeelingLucky.name}."),
     solvers.optSilentErrors -> Description(Solvers, "Fail silently into UNKNOWN when encountering an error"),
     solvers.unrolling.optUnrollBound -> Description(Solvers, "Maximum number of unroll steps to perform"),
     solvers.unrolling.optUnrollFactor -> Description(Solvers, "Number of unrollings to perform between each interaction with the SMT solver"),
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index 53c883c67..b28f85d0a 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -6,6 +6,7 @@ package solvers
 import utils._
 
 object optCheckModels  extends FlagOptionDef("check-models", false)
+object optIgnoreModels extends FlagOptionDef("ignore-models", false)
 object optSilentErrors extends FlagOptionDef("silent-errors", false)
 
 case object DebugSectionSolver extends DebugSection("solver")
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 16c4ff551..77228b8d8 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -123,6 +123,7 @@ abstract class AbstractUnrollingSolver private
   protected final def decode(tpe: t.Type): Type = programEncoder.decode(tpe)
 
   lazy val checkModels = options.findOptionOrDefault(optCheckModels)
+  lazy val ignoreModels = options.findOptionOrDefault(optIgnoreModels)
   lazy val silentErrors = options.findOptionOrDefault(optSilentErrors)
   lazy val unrollBound = options.findOptionOrDefault(optUnrollBound)
   lazy val unrollFactor = options.findOptionOrDefault(optUnrollFactor)
@@ -613,6 +614,9 @@ abstract class AbstractUnrollingSolver private
     inox.Model(program)(exModel.vars, exModel.chooses ++ chooses)
   }
 
+  protected val emptyModel: Model =
+    inox.Model(program)(Map.empty, Map.empty)
+
   def checkAssumptions(config: Configuration)(assumptions: Set[Expr]): config.Response[Model, Assumptions] =
       context.timers.solvers.unrolling.run(scala.util.Try({
 
@@ -685,9 +689,9 @@ abstract class AbstractUnrollingSolver private
         case ModelCheck =>
           reporter.debug(" - Running search...")
 
-          val getModel = !templates.requiresFiniteRangeCheck || checkModels || templates.hasAxioms
-          val checkConfig = config
-            .max(Configuration(model = getModel, unsatAssumptions = unrollAssumptions && templates.canUnroll))
+          val getModel = !templates.requiresFiniteRangeCheck || checkModels || templates.hasAxioms || config.withModel
+          val getAssumptions = (unrollAssumptions && templates.canUnroll) || config.withUnsatAssumptions 
+          val checkConfig = Configuration(model = getModel && !ignoreModels, unsatAssumptions = getAssumptions)
 
           val res: SolverResponse[underlying.Model, Set[underlying.Trees]] = context.timers.solvers.unrolling.check.run {
             underlying.checkAssumptions(checkConfig)(
@@ -705,7 +709,12 @@ abstract class AbstractUnrollingSolver private
               FiniteRangeCheck
 
             case Sat =>
-              CheckResult.cast(Sat)
+              if (config.withModel && ignoreModels) then
+                // did we discard the model check manually?
+                // if yes, recast to the right response, with an empty model
+                CheckResult(config.cast(SatWithModel(emptyModel)))
+              else
+                CheckResult.cast(Sat)
 
             case SatWithModel(model) =>
               Validate(model)
@@ -814,6 +823,31 @@ abstract class AbstractUnrollingSolver private
             Unroll
           }
 
+        case ProofCheck if ignoreModels =>
+          // check without additional model-guidance for unrolling
+          reporter.debug(" - Running search without blocked literals (w/o lucky test)")
+
+          val res = context.timers.solvers.unrolling.check.run {
+              underlying.checkAssumptions(Configuration(model = false, unsatAssumptions = config.withUnsatAssumptions))(
+                encodedAssumptions.toSet ++ templates.refutationAssumptions
+              )
+            }
+
+          reporter.debug(" - Finished search without blocked literals")
+
+          res match {
+            case Abort() =>
+              CheckResult.cast(Unknown)
+
+            case _: Unsatisfiable =>
+              CheckResult.cast(res)
+
+            case _: Satisfiable =>
+              Unroll
+
+            case otherwise => sys.error(s"Unexpected case: $otherwise")
+          }
+
         case ProofCheck =>
           if (feelingLucky) {
             reporter.debug(" - Running search without blocked literals (w/ lucky test)")
@@ -917,7 +951,7 @@ trait UnrollingSolver extends AbstractUnrollingSolver { self =>
     type Model = targetProgram.Model
   }
 
-  override lazy val name = "U:"+underlying.name
+  override lazy val name = "U:" + underlying.name
 
   override val templates = new TemplatesImpl(targetProgram, context)