Hi, the following input in Yices 2.6.4 seems to take a while compared to Z3 and CVC5. Also, Yices 2.5.0 terminates instantly with sat.
(set-logic QF_LIA)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (not (and (<= (mod b (- 968)) (mod b 53)) (= (mod a 533) (- a b)))))
(assert (not (and (<= (div b 432) (div a 492)) (< (- b b) (mod b (- 554))))))
(check-sat)
(exit)
I tested this on both Windows 10 and Ubuntu 18.04.6.
Are there any options that could possibly improve performance?
Hi, the following input in Yices 2.6.4 seems to take a while compared to Z3 and CVC5. Also, Yices 2.5.0 terminates instantly with
sat
.I tested this on both Windows 10 and Ubuntu 18.04.6. Are there any options that could possibly improve performance?
Here are some stats from Yices 2.6.4 with the provided input: ( :num-terms 31 :num-types 4 :total-run-time 812.179 :boolean-variables 62380 :atoms 62379 :clauses 14080 :restarts 23 :clause-db-reduce 61 :clause-db-simplify 0 :decisions 549085 :conflicts 2545836 :theory-conflicts 71951 :boolean-propagations 40119973 :theory-propagations 37910214 :simplex-init-vars 22 :simplex-init-rows 13 :simplex-init-atoms 5 :simplex-vars 260 :simplex-rows 249 :simplex-atoms 62379 :simplex-pivots 61612 :simplex-conflicts 66552 :simplex-interface-lemmas 0 :simplex-integer-vars 40 :simplex-branch-and-bound 61847 :simplex-gomory-cuts 481 :simplex-bound-conflicts 36342 :simplex-bound-recheck-conflicts 6080 :simplex-itest-conflicts 5399 :simplex-itest-bound-conflicts 30943 :simplex-itest-recheck-conflicts 30943 :simplex-gcd-conflicts 0 :simplex-dioph-checks 0 :simplex-dioph-conflicts 0 :simplex-dioph-bound-conflicts 0 :simplex-dioph-recheck-conflicts 0 )