Stop FMB running in ucore mode

vprover · Jul 8, 2021 · 0b42c35 · 0b42c35
1 parent 108158b
commit 0b42c35
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Kernel/MainLoop.cpp b/Kernel/MainLoop.cpp
@@ -119,6 +119,9 @@ MainLoop* MainLoop::createFromOptions(Problem& prb, const Options& opt)
     if(env.statistics->polymorphic || env.statistics->higherOrder){
       USER_ERROR("Finite model buillding is currently not compatible with polymorphism or higher-order constructs");       
     }
+    if(env.options->outputMode() == Shell::Options::Output::UCORE){
+      USER_ERROR("Finite model building is not compatible with producing unsat cores");
+    }
     //TODO should return inappropriate result instead of error
     res = new FiniteModelBuilder(prb,opt);
     break;