diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 2eccba80..d31d65a1 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -990,6 +990,11 @@ module type SOLVER_INTERNAL = sig
       is given the whole trail.
   *)
 
+  val declare_pb_is_incomplete : t -> unit
+  (** Declare that, in some theory, the problem is outside the logic fragment
+      that is decidable (e.g. if we meet proper NIA formulas).
+      The solver will not reply "SAT" from now on. *)
+
   (** {3 Model production} *)
 
   type model_hook =
diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml
index 25153fe5..02f13be9 100644
--- a/src/smt-solver/Sidekick_smt_solver.ml
+++ b/src/smt-solver/Sidekick_smt_solver.ml
@@ -262,6 +262,7 @@ module Make(A : ARG)
       mutable on_partial_check: (t -> theory_actions -> lit Iter.t -> unit) list;
       mutable on_final_check: (t -> theory_actions -> lit Iter.t -> unit) list;
       mutable level: int;
+      mutable complete: bool;
     }
 
     and preprocess_hook =
@@ -633,6 +634,12 @@ module Make(A : ARG)
     let[@inline] final_check (self:t) (acts:_ Sidekick_sat.acts) : unit =
       check_ ~final:true self acts
 
+    let declare_pb_is_incomplete self =
+      if self.complete then (
+        Log.debug 1 "(solver.declare-pb-is-incomplete)";
+      );
+      self.complete <- false
+
     let create ~stat ~proof (tst:Term.store) (ty_st:Ty.store) () : t =
       let rec self = {
         tst;
@@ -658,6 +665,7 @@ module Make(A : ARG)
         on_partial_check=[];
         on_final_check=[];
         level=0;
+        complete=true;
       } in
       ignore (Lazy.force @@ self.cc : CC.t);
       self