3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00

skip optimization

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-16 20:58:30 -08:00
parent c1402ad70f
commit ea778eefb2

View file

@ -245,6 +245,7 @@ namespace opt {
// every time probing whether to include soft_i,
// include suffix that is known to be assignable to T
//
lbool maxlexN() {
unsigned sz = m_soft.size();
for (unsigned i = 0; i < sz; ++i) {
@ -297,7 +298,7 @@ namespace opt {
lbool operator()() override {
init();
return maxlexN();
return maxlex1();
}