我在用着Z3作为一个黑匣子，可以找到与这样的C＃代码的某些现实世界对象的所有可能组合：while(solver.Check()==Status.SATISFIABLE){SATModel=solver.Model;....//inverttheModel....solver.Assert(InvertedModel)}对于我的大多数问题，该程序都可以正常工作，但是现在我有一个更大的问题，在没有约束的情况下，将有8.5e+64可能的组合。我从大约6000个约束开始。我观察到的是，检查动作在开始时需要不到0.02秒，并且缓慢地积累。100000发现解决方案后，每回合已经需要1秒钟，在130000圈