search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

[consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5641

Closed zhendongsu closed 2 years ago

zhendongsu commented 2 years ago 
[562] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/qe/mbp/mbp_arith.cpp
Line: 72
m.limit().is_canceled() || !m.is_false(val)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[563] %
[563] % cat small.smt2
(declare-fun a (Int Int) Int)
(declare-fun b (Int Int Real) (Array Int (Array Int Real)))
(assert (forall ((c Int) (d Int) (e Int) (f Int) (g Real)) (and (= (select (select (b 0 (a e f) g) c) d) g))))
(check-sat)
[564] %
zhendongsu commented 2 years ago 
[525] % z3release small.smt2
sat
[526] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
unexpected SAT
ASSERTION VIOLATION
File: ../src/sat/smt/sat_dual_solver.cpp
Line: 151
UNEXPECTED CODE WAS REACHED.
Z3 4.8.13.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[527] % 
[527] % cat small.smt2
(declare-const a Bool)
(declare-const b Bool)
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(assert (= (and a (> (div (* d e) d) (div (* d e) d))) (and a b)
  (forall ((d Int)) (forall ((e Int)) (and (=> (or (forall ((e Int))
  (and (forall ((c Int)) (= 0 c)) (<= 0 e) (= (* (- (* d e)) e) d c)))
  (= 0 (* d) c)) a (= (= (< d e) (forall ((e Int)) (and a (> c d) (= 0
  c))) (and a b)) (forall ((d Int)) (forall ((e Int)) (> e c))))) a
  (=> (forall ((d Int)) (forall ((e Int)) (and b (= 0 c)))) a (> c
  d)))))))
(check-sat)
[528] %
zhendongsu commented 2 years ago 
[519] % z3release model_validate=true small.smt2
sat
[520] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
failed to verify: (not (and (= n!4 a!val!35) (= o!5 S30!val!0) (= w!6 S14!val!2)))
evaluated to false
(params drat.file null keep_cardinality_constraints true pb.solver solver)
...
[521] % 
[521] % cat small.smt2
(set-option :sat.gc.burst true)
(set-option :rewriter.elim_and true)
(declare-sort g)
(declare-sort t)
(declare-sort S3)
(declare-sort a)
(declare-sort S14)
(declare-sort S15)
(declare-sort b)
(declare-sort p)
(declare-sort S30)
(declare-sort c)
(declare-sort d)
(declare-sort u)
(declare-sort S38)
(declare-sort e)
(declare-fun f () g)
(declare-fun v (S3 t) a)
(declare-fun q (S15 S14) S14)
(declare-fun r (b S14) g)
(declare-fun f22 (p a) b)
(declare-fun h () p)
(declare-fun i () c)
(declare-fun f59 (S30 a) a)
(declare-fun s (d a) t)
(declare-fun j (u d) S30)
(declare-fun k (S38 S3) u)
(declare-fun l () S38)
(declare-fun m (e S30) S15)
(declare-fun f104 () e)
(assert (forall ((n S3) (o d) (w a)) (= (f59 (j (k l n) o) w) (v n (s o w)))))
(assert (forall ((n a) (o S30) (w S14)) (=> (= (r (f22 h n) (q (m f104 o) w)) f) (forall ((qv3 a)) (= (= n (f59 o qv3)) (not (= (r (f22 h qv3) w) f)))) false)))
(check-sat)
[522] %

This doesn't seem to repro any longer. It could be fixed as a side-effect of other changes.

zhendongsu commented 2 years ago 
[515] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/arith_internalize.cpp
Line: 311
!ctx.get_enode(atom)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[516] % cat small.smt2
(declare-fun b () Int)
(declare-fun c (Int Int) Int)
(declare-fun d (Int Int) Int)
(declare-fun q (Int) Int)
(declare-fun f (Int Int Int Int Int Int Int) Int)
(assert (forall ((a Int) (r Int) (g Int) (e Int) (h Int) (j Int) (k Int)) (= (= (f a r g e 0 j k) b) (and (= (q a) h) (forall ((i Int)) (= (c (c e a) i) k))))))
(declare-fun l (Int Int) Int)
(declare-fun m () Int)
(assert (forall ((n Int) (o Int)) (let ((p (l n o))) (= (d (q p) m) b))))
(check-sat)
[517] %
zhendongsu commented 2 years ago 
[569] % z3release small.smt2
sat
[570] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/sat_solver.cpp
Line: 346
Failed to verify: !was_eliminated(lits[i])

Z3 4.8.13.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[571] % 
[571] % cat small.smt2
(set-option :sat.core.minimize true)
(declare-fun a () (_ BitVec 32))
(declare-fun b () (_ BitVec 32))
(declare-fun c () (_ BitVec 32))
(declare-fun e () (_ BitVec 32))
(declare-fun d () (_ BitVec 32))
(define-fun dfoo () Bool (= (= d (bvadd (bvmul a e))) (= true (= true (= (= b (bvadd #x00000001)) (= b c))))))
(assert (not (=> (= (or true (not (= dfoo or))) true) dfoo)))
(check-sat)
[572] %
zhendongsu commented 2 years ago

Not sure whether the following is of interest as the formula is invalid:

[562] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
(error "line 1 column 27: invalid datatype declaration, '(' expected got a")
ASSERTION VIOLATION
File: ../src/util/map.h
Line: 150
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[563] % 
[563] % cat small.smt2
(declare-datatypes ((a 0)))
(declare-fun b () a)
(assert (= b b))
(check-sat)
[564] %
zhendongsu commented 2 years ago 
[538] % z3debug small.smt2
unsat
[539] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
...
ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 615
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[540] % 
[540] % cat small.smt2
(declare-fun a () String)
(assert (xor (exists ((b Int)) (= b 0)) (exists ((b Int)) (= (* (+ (str.len a) 1) b) 0))))
(check-sat)
[541] %

This uses strings. Strings will fail validation code.

rainoftime commented 2 years ago

leak

(declare-sort Loc)
(define-sort SetLoc () (Set Loc))
(declare-sort FldLoc)
(declare-fun null$0 () Loc)
(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool)
(declare-fun next$0 () FldLoc)
(declare-fun sk_FP$0 () SetLoc)
(declare-fun sk_FP_1$0 () SetLoc)
(assert (not (= sk_FP_1$0 sk_FP$0)))
(assert (= sk_FP$0 (union sk_FP_1$0)))
(assert (Btwn$0 next$0 null$0 null$0 null$0))
(assert (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z))))
(check-sat)
parent select:                                                                                                                                                                      [24/1031]
   50: (select sk_FP$0 (array-ext[0] sk_FP_1$0 sk_FP$0))
v2: 26 fx (union[Array[Loc:Bool]] sk_FP_1$0)
v3: 48 fx (array-ext[0] sk_FP_1$0 sk_FP$0)
v4: 49 fx (select sk_FP_1$0 (array-ext[0] sk_FP_1$0 sk_FP$0))
v5: 50 fx (select sk_FP$0 (array-ext[0] sk_FP_1$0 sk_FP$0))
clause:
(Btwn$0 next$0 (:var 2) (:var 1) (:var 0))
clause:
(Btwn$0 next$0 (:var 1) (:var 2) (:var 0))
)

=================================================================
==137559==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 16 byte(s) in 2 object(s) allocated from:
    #0 0x4d6c02 in malloc //llvm-project/compiler-rt/lib/asan/asan_malloc_linux.cpp:145
rainoftime commented 2 years ago

src/sat/smt/euf_internalize.cpp:174

(declare-datatypes ((E 0)) (((one))))
(declare-datatypes ((F 0)) (((four) (five) (six))))
(declare-sort A)
(declare-datatypes ((I 0)) (((c_I (bar1 E) (bar2 Int) (bar3 Int) (bar4 A)))))
(declare-sort B)
(declare-datatypes ((BOOL 0)) (((Truth) (Falsity))))
(declare-sort C)
(declare-datatypes ((J 0)) (((c_J (f1 BOOL) (f2 Int) (f3 Int) (f4 Int) (f5 I) (f6 B) (f7 C)))))
(declare-datatypes ((K 0)) (((c_K (g1 BOOL) (g2 F) (g3 A) (g4 BOOL)))))
(declare-fun e2 () (Array A K))
(declare-fun s2 () (Array A J))
(assert (forall ((x A)) (exists ((e1 (Array A K))) (forall ((s1 (Array A J))) (forall ((y A)) (not (= (ite (not (= (= y (g3 (e1 x))) (=> (= s2 (store s1 y (c_J (f1 (s1 y)) (f2 (s1 y)) (f3 (s1 y)) (f4 (s1 y)) (f5 (s1 y)) (f6 (s1 y)) (f7 (s1 y))))) (forall ((s A)) (= s (g3 (select e2 s))))))) Truth Falsity) Truth)))))))
(check-sat)
ASSERTION VIOLATION
File: ../src/sat/smt/euf_internalize.cpp
Line: 174
m_egraph.find(e)->bool_var() == v
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
rainoftime commented 2 years ago

AddressSanitizer: FPE ../src/sat/smt/q_mbi.cpp:133 in q::mbqi::choose_term(euf::enode*)

(set-option :sat.branching.heuristic chb)
(declare-sort S 0)
(declare-fun f (S S) S)
(declare-fun g (S S) S)
(assert (forall ((a S)) (forall ((b S)) (let (($x27 (forall ((x S) (y S) (z S)) (= (f (f x y) z) (f (f y z) x))))) (let (($x22 (forall ((x S) (y S) (z S)) (! (= (g (g x y) z) (g y z)) :qid k!8)))) (let (($x16 (forall ((x S) (y S)) (= (f (g x y) (g x x)) x)))) (let (($x11 (forall ((x S) (y S)) (! (= (g x (g x x)) x) :qid k!6)))) (and (forall ((x S) (y S)) (= (f x x) x)) $x16 $x22 (forall ((x S) (y S) (z S)) (= (f y z) (f (g y z) x))) (= a (g a b))))))))))
(check-sat)
rainoftime commented 2 years ago

AddressSanitizer: SEGV ../src/ast/ast.h:501

(declare-fun z () Real)
(declare-fun x () Real)
(declare-fun theta () Real)
(assert (forall ((y Real)) (forall ((phi Real)) (and (= y (* (sin theta) (sin phi))) (not (= 0.0 (+ (* y) (* x z))))))))
(check-sat)
NikolajBjorner commented 2 years ago

OK, thanks. These are always good. Note that I can also, or at least did not have much trouble to, break the new core by running smtlib benchmarks directly. There is also a more fundamental problem with relevancy in the new core which will likely require a heavy revision.

NikolajBjorner commented 2 years ago

Commit:84ddd06 OS: Ubuntu 20.04

$ z3 delta.smt2
unsat
$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
unexpected SAT
ASSERTION VIOLATION
File: ../src/sat/smt/sat_dual_solver.cpp
Line: 152
UNEXPECTED CODE WAS REACHED.
Z3 4.8.14.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
$ cat delta.smt2
(declare-const v (_ BitVec 4))
(declare-const _v (_ BitVec 4))
(declare-const x Bool)
(declare-const x6 Bool)
(assert (and (forall ((VA (_ BitVec 8)) (VA (_ BitVec 8)) (V (_ BitVec 8)) (V (_ BitVec 8)) (V (_ BitVec 8)) (VA (_ BitVec 8)) (V (_ BitVec 8)) (A (_ BitVec 8)) (V (_ BitVec 8))) (not (ite (distinct false (forall ((A (_ BitVec 8))) false)) false (= (bvlshr V VA) ((_ zero_extend 4) _v))))) (forall ((V (_ BitVec 8))) (or (not (distinct false (forall ((A (_ BitVec 8))) (not (= V (bvlshr A ((_ zero_extend 4) v))))))) (ite x6 (distinct false (forall ((VA (_ BitVec 8))) (not (= (bvlshr V VA) (_ bv0 8))))) (distinct x (distinct (forall ((A (_ BitVec 8))) (= V (bvlshr (_ bv0 8) (_ bv1 8)))) (forall ((V (_ BitVec 8))) (not (= V (bvlshr (_ bv0 8) (_ bv0 8))))))))))))
(check-sat)
merlinsun commented 2 years ago

Commit: 6b0dc6d OS: Ubuntu 20.04

$ z3 delta.smt2
unsat
$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
Segmentation fault (core dumped)
$ cat delta.smt2
(assert (forall ((V Float16)) (= ((_ to_fp 5 11) RTN 65535.0 0) (fp (_ bv0 1) (_ bv0 5) (_ bv0 10)))))
(check-sat)

@wintersteiger - there is maybe an assumption that pre-processing simplification avoids the code path that gets hit here. When using default_tactic=smt there is limited pre-processing. fpa2bv_converter.cpp calls mk_numeral in line 2827 for some expression that isn't a numeral. The expression is created a few lines above. Looking at fpa_decl_plugin.cpp we see that the mk_numeral method in the plugin does not always create expressions with one parameter. This is the case for NaN and +/- infinity.

NikolajBjorner commented 2 years ago

First of all, I wish you a Merry Christmas!

This is a bug related to (check-sat-using (then sat default)).

OS: ubuntu 20.04 Commit: 6b0dc6d

$ z3 case.smt2
sat
$ z3 case_tactic.smt2 tactic.default_tactic=smt sat.euf=true
unsat
$ z3 case_tactic.smt2
unknown
$ z3 case.smt2 tactic.default_tactic=smt sat.euf=true
unknown
$ z3 case_tactic.smt2 tactic.default_tactic=smt sat.euf=true
unsat
$ cat case.smt2
(declare-fun var4 () (_ FloatingPoint 2 3))
(declare-fun var2 () RoundingMode)
(declare-fun var1 () (_ FloatingPoint 11 53))
(declare-fun var0 () RoundingMode)
(assert (or (= var4 (fp.max (_ -zero 2 3) (fp.max (_ +zero 2 3) (_ -zero 2 3)))) (= ((_ to_fp 11 53) var0 (/ 88722839111672996637.0 125000000000000000.0)) var1) (= ((_ to_fp 11 53) var0 (/ 88722839111672996637.0 125000000000000000.0)) var1) (fp.isZero var4) (= var4 (fp.max (_ -zero 2 3) (fp.max (_ +zero 2 3) (_ -zero 2 3)))) (= ((_ to_fp 11 53) var0 (/ 88722839111672996637.0 125000000000000000.0)) var1)))
(check-sat)
$ cat case_tactic.smt2
(declare-fun var4 () (_ FloatingPoint 2 3))
(declare-fun var2 () RoundingMode)
(declare-fun var1 () (_ FloatingPoint 11 53))
(declare-fun var0 () RoundingMode)
(assert (or (= var4 (fp.max (_ -zero 2 3) (fp.max (_ +zero 2 3) (_ -zero 2 3)))) (= ((_ to_fp 11 53) var0 (/ 88722839111672996637.0 125000000000000000.0)) var1) (= ((_ to_fp 11 53) var0 (/ 88722839111672996637.0 125000000000000000.0)) var1) (fp.isZero var4) (= var4 (fp.max (_ -zero 2 3) (fp.max (_ +zero 2 3) (_ -zero 2 3)))) (= ((_ to_fp 11 53) var0 (/ 88722839111672996637.0 125000000000000000.0)) var1)))
(check-sat-using (then sat default))
NikolajBjorner commented 2 years ago

The remaining bugs are related to FP. The last one is not easy to debug: it dumps the state of the solver after an inconclusive round and then calls the solver again with the state. At that point it reports unsat. The issue is likely specific to floating points. It would have to be addressed in tandem with other FP issues.

NikolajBjorner commented 2 years ago

Move FP bugs to #4889