Is this expression really unsat?

Question

I was debugging my code, then I encountered that z3 says this expression is unsat

(and (not (>= s 13))
     (>= s 0)
     (>= 13 s)
     (>= pc0_thread1 0)
     (>= pc1_thread1 0)
     (>= pc2_thread1 0)
     (>= pc3_thread1 0)
     (>= pc4_thread1 0)
     (>= pc0_main 0)
     (>= pc0_thread2 0)
     (>= pc1_thread2 0)
     (= 1 pc0_main))

I was surprised and tried to use the unsat_core function but it returns an empty array. Am I missing something?

Answer 1

My mistake was that I was using the "solver" in a loop, but I wasn't resetting each time, so it had the information from previous loop iterations, thus producing the wrong results. After printing solver.assertions(), I figured out what is happening!

Thank you all.

Answer 2

I am obtaining "sat"

(declare-fun s () Real)
(declare-fun pc0_thread1 () Real)
(declare-fun pc1_thread1 () Real)
(declare-fun pc2_thread1 () Real)
(declare-fun pc3_thread1 () Real)
(declare-fun pc4_thread1 () Real)
(declare-fun pc0_main () Real)
(declare-fun pc0_thread2 () Real)
(declare-fun pc1_thread2 () Real)
(assert (and (not (>= s 13))
 (>= s 0)
 (>= 13 s)
 (>= pc0_thread1 0)
 (>= pc1_thread1 0)
 (>= pc2_thread1 0)
 (>= pc3_thread1 0)
 (>= pc4_thread1 0)
 (>= pc0_main 0)
 (>= pc0_thread2 0)
 (>= pc1_thread2 0)
 (= 1 pc0_main)))

(check-sat)

Run this example online here

Answer 3

Like Juan, I get SAT, but I've tried it with integers:

(declare-const s Int)
(declare-const pc0_thread1 Int)
(declare-const pc1_thread1 Int)
(declare-const pc2_thread1 Int)
(declare-const pc3_thread1 Int)
(declare-const pc4_thread1 Int)
(declare-const pc0_main Int)
(declare-const pc0_thread2 Int)
(declare-const pc1_thread2 Int)

(assert (and (not (>= s 13))
  (>= s 0)
  (>= 13 s)
  (>= pc0_thread1 0)
  (>= pc1_thread1 0)
  (>= pc2_thread1 0)
  (>= pc3_thread1 0)
  (>= pc4_thread1 0)
  (>= pc0_main 0)
  (>= pc0_thread2 0)
  (>= pc1_thread2 0)
  (= 1 pc0_main))
)

(check-sat)

Zeinab: I presume you're not using the SMT2 frontend, but the API. Could you give us more information as to what you're doing with this expression? For instance, we recently had a bug report about the ctx-solver-simplify tactic delivering wrong results (see here), but I would have to know exactly what your goals look like and which tactics you're applying.