Assume that I have a Z3 preamble that includes several function declarations and definitional axioms (with explicit patterns), e.g., my own sequence axioms:
(declare-sort $Seq)
(declare-fun $Seq.nil () $Seq)
(declare-fun $Seq.len ($Seq) Int)
(declare-fun $Seq.con (Int $Seq) $Seq)
(declare-fun $Seq.at ($Seq Int) Int)
(declare-fun $Seq.in ($Seq Int) Bool)
...
(assert (forall ((xs $Seq)) (! ... )
(assert (forall ((xs $Seq) (x Int)) (! ... )
...
After this preamble has been emitted a lot of assertions are pushed to Z3, interspersed with calls to check-set to see whether certain negated formulas can be shown unsat (FYI: my context is software verification using symbolic execution).
Most of these assertions are simple and don't refuting them doesn't require the sequence axioms. However, from a few simple tests I get the impression that their presence nevertheless slows Z3 down.
I thus guarded the definitional axioms by an implication with a dummy boolean constant as the left-hand side of the implication (as suggested by this answer), e.g.,
(declare-const $useSeq Bool)
(assert (=> ($useSeq (forall ((xs $Seq)) (! ... )
and changed every check-sat that needs to reason about sequences into one that assumes $useSeq, i.e.,
(check-sat $useSeq)
Question: Is there a tactic/way to make Z3 use certain assertions only after a time-out? E.g.,
(check-sat-using (or-else (try-for smt 500) (smt $useSeq)))
I could of course manually emit a time-bounded check-sat first, followed by a check-sat useSeq $useSeq if needed, but it would be nice if it could be done with some kind of tactics.
