[Consolidated] Bugs related to tactics

[muchang]

Assertion violation at ../src/smt/smt_conflict_resolution.cpp Line: 807

[592] % z3release small.smt2
Segmentation fault
[593] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/smt/smt_conflict_resolution.cpp
Line: 807
m_ctx.is_true(n2) || m_ctx.is_false(n2)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[594] % 
[594] % cat small.smt2
(set-option :smt.phase_selection 5)
(set-option :proof true)
(set-option :rewriter.bit2bool false)

(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun b () (_ BitVec 32))
(declare-fun c () (_ BitVec 32))
(assert (let ((d (store (store (store (store a (bvadd (bvshl (bvsub c
    (_ bv4 32)) (_ bv4 32)) (_ bv3 32)) ((_ extract 7 0) b)) (bvadd
    (bvshl (bvsub c (_ bv4 32)) (_ bv4 32)) (_ bv2 32)) ((_ extract 7
    0) (bvsdiv b (_ bv16 32)))) (bvsdiv (bvshl (bvsub c (_ bv4 32)) (_
    bv4 32)) (_ bv1 32)) ((_ extract 7 0) (bvlshr b (_ bv8 32))))
    (bvxnor (bvshl (bvsub c (_ bv4 32)) (_ bv4 32))) ((_ extract 7 0)
    b)))) (= (_ bv1 1) (ite (= (bvudiv (bvor (bvxor (_ bv16 32)))
    (bvshl (concat (_ bv0 24) (select a (bvsub c (_ bv3 32)))) (_ bv24
    32))) (bvnor (bvshl (bvor (bvshl (concat (_ bv0 24) (d (bvadd
    (bvlshr (bvsub c (_ bv4 32)) (_ bv4 32)) (_ bv1 32)))) (_ bv8
    32))) (bvshl (concat (_ bv0 24) (d (bvadd (bvlshr (bvsub c (_ bv4
    32)) (_ bv4 32)) (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0
    24) (d (bvadd (bvlshr (bvsub c (_ bv4 32)) (_ bv4 32)) (_ bv3
    32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1)))))
(check-sat-using smt)
[595] % 

Commit: 4db41c0

[muchang]

(bv) Assertion violation at ../src/smt/smt_conflict_resolution.cpp Line: 807

[612] % z3release small.smt2
Segmentation fault
[613] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/smt/smt_conflict_resolution.cpp
Line: 807
m_ctx.is_true(n2) || m_ctx.is_false(n2)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[614] % 
[614] % cat small.smt2
(set-option :proof true)
(declare-fun a () (_ BitVec 8))
(declare-fun b () (_ BitVec 8))
(declare-fun c () (_ BitVec 8))
(declare-fun d () (_ BitVec 8))
(assert
 (let ((e ((_ zero_extend 24) a)) (f ((_ zero_extend 24) (_ bv1 8))) (g ((_ zero_extend 24) b)))
  (let ((h (bvsub g (_ bv48 32))) (i ((_ zero_extend 24) c)))
   (let ((j (bvsub (bvadd i (bvshl (bvadd h) f)) (_ bv48 32))))
    (let ((k (bvadd e (bvshl (bvadd j) f))))
     (let ((l (bvsub k (_ bv48 32))) (m ((_ zero_extend 24) d)))
      (and (= (bvsub k (_ bv37 32)) (_ bv1 32))
       (bvule (bvsub m (_ bv40 32)) (_ bv85 32))
       (not (= (bvsub k (_ bv45 32)) (_ bv1 32)))
       (bvsle (_ bv0 32) l))))))))
(check-sat-using bv)
[615] % 

Commit: 4db41c0

[muchang]

(qffd smt) Invalid model on QF_LIA fomula

[628] % z3release model_validate=true small.smt2
sat
(error "line 6 column 32: an invalid model was generated")
(
  ;; universe for (_ bv 2):
  ;;   bv!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!0 () (_ bv 2))
  ;; cardinality constraint:
  (forall ((x (_ bv 2))) (= x bv!val!0))
  ;; -----------
  (define-fun b () Int
    0)
  (define-fun bv () (_ bv 2)
    #b01)
  (define-fun a () Int
    0)
)
[629] % 
[629] % cat small.smt2
(set-logic AUFLIA)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (< 0 b 2))
(assert (= (+ a b) a))
(check-sat-using (then qffd smt))
(get-model)
[630] % 

Commit: 4db41c0

[muchang]

(add-bounds dom-simplify qffd smt) Invalid model on QF_LIA formula

[637] % z3release model_validate=true small.smt2
sat
(error "line 10 column 56: an invalid model was generated")
(
  ;; universe for (_ bv 3):
  ;;   bv!val!2 bv!val!0 bv!val!1 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!2 () (_ bv 3))
  (declare-fun bv!val!0 () (_ bv 3))
  (declare-fun bv!val!1 () (_ bv 3))
  ;; cardinality constraint:
  (forall ((x (_ bv 3))) (or (= x bv!val!2) (= x bv!val!0) (= x bv!val!1)))
  ;; -----------
  ;; universe for (_ bv 5):
  ;;   bv!val!3 bv!val!1 bv!val!2 bv!val!0 bv!val!4 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!3 () (_ bv 5))
  (declare-fun bv!val!1 () (_ bv 5))
  (declare-fun bv!val!2 () (_ bv 5))
  (declare-fun bv!val!0 () (_ bv 5))
  (declare-fun bv!val!4 () (_ bv 5))
  ;; cardinality constraint:
  (forall ((x (_ bv 5)))
          (or (= x bv!val!3)
              (= x bv!val!1)
              (= x bv!val!2)
              (= x bv!val!0)
              (= x bv!val!4)))
  ;; -----------
  ;; universe for (_ bv 4):
  ;;   bv!val!0 bv!val!1 bv!val!2 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!0 () (_ bv 4))
  (declare-fun bv!val!1 () (_ bv 4))
  (declare-fun bv!val!2 () (_ bv 4))
  ;; cardinality constraint:
  (forall ((x (_ bv 4))) (or (= x bv!val!0) (= x bv!val!1) (= x bv!val!2)))
  ;; -----------
  (define-fun a () Int
    (- 2))
  (define-fun d () Int
    0)
  (define-fun bv () (_ bv 5)
    #b11101)
  (define-fun e () Int
    0)
  (define-fun c () Int
    (- 2))
  (define-fun b () Int
    0)
  (define-fun bv () (_ bv 1)
    #b0)
  (define-fun bv () (_ bv 5)
    #b00010)
  (define-fun bv () (_ bv 3)
    #b100)
)
[638] % cat small.smt2
(set-logic AUFNIRA)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(assert (= d b))
(assert (<= e a))
(assert (= c a))
(check-sat-using (then add-bounds dom-simplify qffd smt))
(get-model)
[639] % 

Commit: 4db41c0

[muchang]

(purify-arith qffd smt) Invalid model on QF_UFLIA formula

[677] % z3release model_validate=true small.smt2
sat
(error "line 9 column 45: an invalid model was generated")
(
  ;; universe for (_ bv 3):
  ;;   bv!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!0 () (_ bv 3))
  ;; cardinality constraint:
  (forall ((x (_ bv 3))) (= x bv!val!0))
  ;; -----------
  (define-fun bv () (_ bv 3)
    #b010)
  (define-fun a () Int
    (- 35892))
  (define-fun b ((x!0 Int)) Bool
    (= x!0 (- 2)))
  (define-fun c ((x!0 Int)) Bool
    (ite (= x!0 0) false
      true))
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 (- 35892)) (= x!1 2)) (- 17945)
      0))
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 (- 35892)) (= x!1 2)) (- 2)
      0))
)
[678] % 
[678] % cat small.smt2
(set-logic AUFNIRA)
(set-option :smt.random_seed 4)
(declare-fun a () Int)
(declare-fun b (Int) Bool)
(declare-fun c (Int) Bool)
(assert (c a))
(assert (= (b 0) (c 0)))
(assert (b (mod a 2)))
(check-sat-using (then purify-arith qffd smt))
(get-model)
[679] % 

Commit: 4db41c0

[muchang]

(purify-arith qffd default) Invalid model on QF_NIRA formula

[708] % z3release model_validate=true small.smt2
sat
(error "line 4 column 49: an invalid model was generated")
(
  ;; universe for (_ bv 3):
  ;;   bv!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!0 () (_ bv 3))
  ;; cardinality constraint:
  (forall ((x (_ bv 3))) (= x bv!val!0))
  ;; -----------
  (define-fun a () Real
    (- 3.0))
  (define-fun bv () (_ bv 3)
    #b010)
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 7) (= x!1 (- 3))) (- 2)
      0))
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 (- 2)) (= x!1 2)) (- 2)
    (ite (and (= x!0 7) (= x!1 (- 3))) 1
      0)))
)
[709] % 
[709] % cat small.smt2
(set-logic AUFNIRA)
(declare-fun a () Real)
(assert (= (* (div 7 a 2)) 0))
(check-sat-using (then purify-arith qffd default))
(get-model)
[710] % 

Commit: 4db41c0

[muchang]

(qffd smt) Invalid model on QF_UFLIA formula

[745] % z3release model_validate=true small.smt2
sat
(error "line 10 column 32: an invalid model was generated")
(
  (define-fun b () Bool
    true)
  (define-fun a () Int
    1)
  (define-fun bv () (_ bv 1)
    #b0)
  (define-fun bv () (_ bv 2)
    #b00)
  (define-fun f () Bool
    false)
  (define-fun c () Bool
    false)
  (define-fun d () Bool
    false)
  (define-fun g () Bool
    false)
  (define-fun e ((x!0 Int)) Int
    1)
)
[746] % 
[746] % cat small.smt2
(set-logic AUFNIRA)
(declare-fun a () Int)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun e (Int) Int)
(declare-fun f () Bool)
(declare-fun g () Bool)
(assert (= (ite (= a 0) 0 (ite b 0 (ite c 0 (ite d 0 (ite g (ite f 1 0) 0))))) (e 0) a 1))
(check-sat-using (then qffd smt))
(get-model)
[747] % 

Commit: 4db41c0

[muchang]

(qffd smt) Solution soundness bug in QF_LIA

[759] % z3release small.smt2
unsat
sat
[760] % 
[760] % cat small.smt2
(set-logic AUFNIRA)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (or (= a 0) (= a 1)))
(assert (= a (- b)))
(assert (> b 0))
(check-sat)
(check-sat-using (then qffd smt))
[761] % 

Commit: 4db41c0

[muchang]

(simplify qffd smt) Invalid model in QF_UFLIA

[775] % z3release model_validate=true small.smt2
sat
(error "line 7 column 41: an invalid model was generated")
(
  ;; universe for (_ bv 3):
  ;;   bv!val!0 bv!val!1 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!0 () (_ bv 3))
  (declare-fun bv!val!1 () (_ bv 3))
  ;; cardinality constraint:
  (forall ((x (_ bv 3))) (or (= x bv!val!0) (= x bv!val!1)))
  ;; -----------
  ;; universe for (_ bv 2):
  ;;   bv!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!0 () (_ bv 2))
  ;; cardinality constraint:
  (forall ((x (_ bv 2))) (= x bv!val!0))
  ;; -----------
  (define-fun bv () (_ bv 2)
    #b00)
  (define-fun bv () (_ bv 3)
    #b001)
  (define-fun a () Int
    0)
  (define-fun bv () (_ bv 1)
    #b0)
  (define-fun bv () (_ bv 3)
    #b110)
  (define-fun b ((x!0 Int)) Int
    0)
)
[776] % 
[776] % cat small.smt2
(set-logic AUFNIRA)
(set-option :rewriter.eq2ineq true)
(declare-fun a () Int)
(declare-fun b (Int) Int)
(assert (= a 1))
(assert (= (b 0) a))
(check-sat-using (then simplify qffd smt))
(get-model)
[777] %

Commit: 4db41c0

[muchang]

(purify-arith ctx-solver-simplify) Assertion violation at ../src/smt/smt_context.cpp Line: 942

[846] % z3release small.smt2
(smt.diff_logic: non-diff logic expression (mod (* (- 1) g) g))
Segmentation fault
[847] % z3debug small.smt2
(smt.diff_logic: non-diff logic expression (mod (* (- 1) g) g))
ASSERTION VIOLATION
File: ../src/smt/smt_context.cpp
Line: 942
parent->is_cgr()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[848] % cat small.smt2
(set-option :smt.arith.solver 3)
(declare-fun d (Int) Int) 
(declare-fun intand (Int Int Int) Int) 
(define-fun c ((g Int) (a Int)) Int (* a (d (- g 1))))   
(define-fun j ((g Int) (k Int)) Bool (>= k 0  )) 
(define-fun e ((g Int) (a Int) (b Int)) Int (ite (= b 0) a (mod a b))) 
(define-fun f ((g Int) (a Int)) Int (e g (-   g ) g  )) 
(define-fun intmins ((g Int)) Int (d (- g 1)))  
(define-fun h ((g Int) (a Int) (b Int)) Bool (< g b )) 
(define-fun i ((g Int) (a Int) (b Int)) Bool (=    a  0)) 
(define-fun p ((g Int)) Bool 
(forall ((a Int) (b Int)) (= (and (j g a) (j g b)) (= (intand g a b)  0 (c g b))))) 
(define-fun q ((g Int)) Bool 
(exists ((a Int)) (= (intand g a a) a))) 
(define-fun m ((g Int)) Bool (q g)) 
(define-fun r ((g Int)) Bool (and (p g) (m g))) 
(define-fun l ((g Int) (k Int) (s Int) (t Int)) Bool (i g (e g k s) t)) 
(define-fun n ((g Int) (s Int) (t Int)) Bool (h g   g  (intand g (f g s) t))) 
(declare-fun g () Int) 
(declare-fun s () Int) 
(declare-fun t () Int) 
(define-fun inv ((g Int) (s Int) (t Int)) Int (intand g t (intmins g))) 
(define-fun o ((g Int) (s Int) (t Int)) Bool (l g (inv g s t) s t)) 
(define-fun u ((g Int) (s Int) (t Int)) Bool (=(n g s t) (o g s t))) 
(define-fun v () Bool   (u g s t))  
(assert (r g)) 
(assert v)
(check-sat-using (then purify-arith ctx-solver-simplify))
[849] % 

Commit: 4db41c0

[muchang]

(sat-preprocess default) Assertion violation at ../src/tactic/generic_model_converter.h Line: 51

[875] % z3debug small.smt2
sat
ASSERTION VIOLATION
File: ../src/tactic/generic_model_converter.h
Line: 51
is_app(d) && to_app(d)->get_num_args() == 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[876] % 
[876] % cat small.smt2
(declare-fun a () String)
(assert (= (str.suffixof "A" (str.replace "" a "")) (= a "")))
(check-sat)
(check-sat-using (then sat-preprocess default))
[877] % 

Commit: 4db41c0

[muchang]

(purify-arith smt) Assertion violation at ../src/model/func_interp.cpp Line: 211

[898] % z3debug small.smt2
sat
ASSERTION VIOLATION
File: ../src/model/func_interp.cpp
Line: 211
get_entry(args) == nullptr
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[899] % cat small.smt2
(set-option :rewriter.arith_lhs true)
(set-option :nlsat.reorder false)
(set-option :proof true)
(set-option :smt.random_seed 9)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(assert (forall ((g Real)) (= (>= (div (- (/ (* e e) (- 2 d))) (/ (mod b b) (- 2 d))) 0) (= g a (mod c g) f g))))
(check-sat)
(check-sat-using (then purify-arith smt))
[900] % 

Commit: 4db41c0

[muchang]

(purify-arith reduce-invertible smt) Refutation soundness bug on QF_BV

[913] % z3release small.smt2
sat
unsat
[914] % cat small.smt2
(declare-fun a () (_ BitVec 2))
(declare-fun b () (_ BitVec 2))
(assert (= (bvsmod (bvadd (bvneg b) b) b) (bvshl (bvnot (bvmul a a)) b)))
(check-sat)
(check-sat-using (then purify-arith reduce-invertible smt))
[915] % 

Commit: 4db41c0

[NikolajBjorner]

To save bandwidth for something more useful I will not be dealing with qffd "abuse" issues.

[NikolajBjorner]

The remaining is
#4932 (comment)
Others are resolved.

[muchang]

(purify-arith add-bounds lia) Assertion violation at ../src/ast/ast.cpp Line: 432

(set-option :proof true)
(declare-fun a (Int) Bool)
(declare-fun h (Int) Int)
(define-fun b () Bool (and (= (h 0) (h 2) 4) (= (h 3) 8)))
(define-fun c () Bool
(forall ((i Int) (j Int)) (or (>= i 0) (= (<= i j) (= (h i) j )))))
(define-fun d () Bool
(forall ((i Int) (j Int) (n Int)) (< i j)))
(define-fun l () Bool
(forall ((k Int) (n Int)) (and (>= k 1) (distinct (- (h k) 1) (/ 2 n)))))
(define-fun e () Bool
(forall ((k Int)) (! (=> (>= k 0) (>= (h k) 1)) :pattern (a k))))
(define-fun f () Bool
(forall ((k Int)) (! (=> (>= k 0) (= (div k (h k)) 0)) :pattern (a k))))
(assert (xor b c d l e f))
(check-sat-using (then purify-arith add-bounds lia))

Adding "(check-sat)" before the check-sat-using hides the bug.

Commit: 8abb644

[muchang]

(purify-arith ctx-solver-simplify) Segmentation fault on ALIA formula

[542] % z3release small.smt2
Segmentation fault
[543] % 
[543] % cat small.smt2
(set-option :rewriter.expand_nested_stores true)
(set-option :model_evaluator.completion true)
(declare-fun id_ds1_filter_init () (Array Int (Array Int Real)))
(declare-fun a () Real)
(declare-fun h () (Array Int (Array Int Real)))
(declare-fun pv63 () Int)
(declare-fun g () (Array Int (Array Int Real)))
(declare-fun i (Int Real) (Array Int Real))
(assert (forall ((?k Int) (?j Real)) (= (select (i 0 ?j) ?k) ?j )))
(assert (not (=> (forall ((?b Int) (?c Int)) (=> (>= ?b 0) (<= ?b 5)
 (= (select (select g ?b) ?c) a))) (forall ((?l Int) (?d Int)) (=>
 (>= ?d 5 ) (= (select (select h ?l) ?d) a))) (forall ((?m Int) (?n
 Int)) (let ((?e 0)) (= (and (>= ?m ?e)) (=(< ?m pv63) (= (select
 (select id_ds1_filter_init ?m) ?n) a))))) (forall ((?o Int) (?f
 Int)) (=> (>= ?o 0) (<= ?o 2) (<= ?f 2) (= 0 a))))))
(check-sat-using (then purify-arith ctx-solver-simplify))
[544] %

Commit: 8abb644