(check-sat) vs (check-sat-using smt)

Question

After reading the strategies guide of Z3, and this answer by Leo, I expected that (check-sat) and (check-sat-using smt) are equivalent. However, when running Z3 4.3.2 three times against our test suite (230 SMTLIB2 files), it took 198s/192s/195s seconds with (check-sat), but 275s/283s/270s with (check-sat-using smt). I also tried the nightly build Z3 4.4.0 d3fb5f2a4cda, and the difference was similar.

Why might that be?

A bit more information that might be relevant:

Windows 7 x64, Z3 x64
All our tests are configured with auto_config false and smt.mbqi false
All use quantifiers and uninterpreted functions
Some use (non-linear) int and/or real arithmetic
All make heavy use of push-pop blocks

Edit: What I ultimately would like to do is to set a timeout for some check-sat calls, but not for all. AFAIK, this is not possible with check-sat itself, but check-sat-using (using-params smt :soft_timeout $timeout) should work. Is that right?

Looks as if stackoverflow.com/questions/23973453 were potentially related — Malte Schwerhoff
FYI in the current master branch of Z3, it's possible to get the effect you're looking for using (check-sat-using default). See this question. — Douglas B. Staple

Christoph Wintersteiger Christoph Wintersteiger · Accepted Answer · 2015-02-19T14:16:46

I assume you're running Z3 on an SMT2 file?

Z3 has facilities for determining the logic of the benchmark when none is specified (see e.g., default_tactic.cpp). The smt tactic is the fallback when no other tactic applies. When Z3 is run with -v:10, it will show which (sub)-tactic is run.

In the recent past we also had some problems with configuration parameters not making it through to the smt kernel. We've fixed those, but it's of course possible that there's still a bug somewhere.

(check-sat) vs (check-sat-using smt)

1 Answers