[consolidated] issues with new core #6429

zhendongsu · 2022-10-29T08:11:39Z

[528] % z3debug small.smt2
unsat
[529] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 479
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[530] % cat small.smt2
(declare-fun a () Int)
(assert (forall ((b Int)) (= (mod (+ (mod b 4) a) 4) 2)))
(check-sat)

The text was updated successfully, but these errors were encountered:

zhendongsu · 2022-10-30T08:28:23Z

[554] % z3debug small.smt2
sat
[555] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/qe/qsat.cpp
Line: 636
validate_defs("check_sat")
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[556] % cat small.smt2
(set-option :sat.prob_search true)
(define-sort a () (_ FloatingPoint 8 4))
(declare-fun b () a)
(assert (distinct (forall ((c a)) (distinct (fp.abs c) b))))
(check-sat-using (then purify-arith nra qe2))

zhendongsu · 2022-10-30T13:52:49Z

[529] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Failed to validate 76 147: (= (extract[31:31] (bv_wrap a)) (extract[31:31] (bv_wrap #80))) true
(sat
...
[530] % cat small.smt2
(declare-fun a () Float32)
(assert (forall ((b Float32)) (not (fp.isPositive (fp.max a b)))))
(check-sat)

zhendongsu · 2022-10-30T15:41:14Z

[672] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
(let ((a!1 (* (- 1) (ite (>= (pow2 j!23) 0) 1 (- 1)) (pow2 j!23))))
(let ((a!2 (+ (mod (+ x!24 (pow2 i!22)) (pow2 j!23)) a!1)))
  (pow2 a!2))) := 1
(pow2 j!86) := 8
(let ((a!1 (* (- 1) (ite (>= (pow2 j!23) 0) 1 (- 1)) (pow2 j!23))))
(let ((a!2 (+ (mod (+ x!24 (pow2 i!22)) (pow2 j!23)) a!1)))
  (pow2 a!2))) -> ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 168
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[673] % z3debug model_validate=true small.smt2
sat
[674] % cat small.smt2
(set-option :smt.ematching false)
(set-option :rewriter.push_ite_arith true)
(set-option :smt.arith.ignore_int true)
(declare-fun pow2 (Int) Int)
(define-fun bitof ((pow2 Int) (false Int) (a Int)) Int 0)
(define-fun pow2_strong_monotinicity () Bool (forall ((i Int) (j Int)) (or (and (<= i 0) (> j 0)) (or (not (< i j)) (distinct (pow2 i) (pow2 j))))))
(define-fun pow2_properties () Bool (and (= (pow2 0) 1) (= 2 (pow2 1)) (= 4 (pow2 0)) (= (pow2 3) 8)))
(declare-fun k () Int)
(declare-fun s () Int)
(declare-fun t () Int)
(declare-const x179__fresh Bool)
(declare-const x220__fresh Bool)
(assert (>= k 1))
(assert (>= s (- (pow2 k) 1)))
(assert (>= t 0))
(assert (<= t (- (pow2 k) 1)))
(assert (or (and (= (pow2 0) 1) (forall ((i Int)) x179__fresh))
         (and (and (= (pow2 0) 1) (= 2 (pow2 1)) (= 4 (pow2 0)) (= (pow2 3) 8))
          x220__fresh
          (forall ((i Int) (j Int)) (or (and (<= i 0) (> j 0)) (or (not (< i j)) (distinct (pow2 i) (pow2 j)))))
          (forall ((i Int) (j Int) (x Int)) (=> (and (>= j 0) (<= x 0) (distinct (mod (+ x (pow2 i)) (pow2 j)) 0)) (< i j)))
          (forall ((k Int) (x Int)) (or (not (>= x 0)) (distinct (- (pow2 k) 1) (* 2 x))))
          (forall ((k Int)) (not (>= k 0))))))
(check-sat-using (then purify-arith ctx-solver-simplify qflra))

zhendongsu · 2022-10-31T11:57:28Z

[521] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1195
m_columns_with_changed_bounds.empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[522] % cat small.smt2
(set-option :smt.arith.ignore_int true)
(set-option :smt.ematching false)
(declare-fun a (Int) Int)
(define-fun b ((c Int) (d Int)) Bool (and (= d 0) (= (a 0) 1) (forall ((e Int)) (= (> e 0) (= (a e) (* (a (- e 1)) 2))))))
(declare-fun c () Int)
(declare-fun f () Int)
(assert (> c 1))
(assert (b c f))
(check-sat)

zhendongsu · 2022-11-02T08:50:12Z

[559] % z3release small.smt2
sat
[560] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Failed to validate 47 283: (<= (+ b (* -1.0 #254)) 0.0) false
(sat
...
[561] % cat small.smt2
(set-option :rewriter.arith_lhs true)
(set-option :rewriter.elim_and true)
(set-option :rewriter.sort_sums true)
(declare-fun a () Int)
(declare-fun b () Real)
(declare-fun c () (Array Int (Array Int Real)))
(declare-fun d (Int Int) Int)
(declare-fun e (Int Int Real) (Array Int (Array Int Real)))
(assert (exists ((f Real)) (and (forall ((j Int) (g Int)) (or (> g a)
  (= b (select (select c j) g)))) (not (exists ((h Int)) (and (>= a 0)
  (distinct b (select (select (e 0 (d 0 0) 0.0) h) h))))) (forall ((i
  Int)) (not (and (>= i 0 i) (distinct 1.0 (select (select (e (d 0 0) 0
  0.0) i) i))))) (distinct b (select (select (store (e 0.0 0 0) 1
  (store (select (e 0.0 0 0) 1) 0 1.0)) 1) 0)))))
(check-sat)

zhendongsu · 2022-11-03T09:21:46Z

[535] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 479
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[536] % cat small.smt2
(assert (forall ((a Int) (b Int) (c Int) (d Int)) (not (= (mod (+ (- a b (mod c 2)) d) 3) 0))))
(check-sat)

* Added function to select the next variable to split on * Fixed typo * Small fixes * uint -> int * Fixed missing assignment for binary clauses * Memory leak in .NET user-propagator The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically * Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation * Update (not compiling yet) * #6429 * remove ternary clause optimization Removing ternary clause optimization from sat_solver simplifies special case handling of ternary clauses throughout the sat solver and dependent solvers (pb_solver). Benchmarking on QF_BV suggests the ternary clause optimization does not have any effect. While removing ternary clause optimization two bugs in unit propagation were also uncovered: it missed propagations when the only a single undef literal remained in the non-watched literals and it did not update blocked literals in cases where it could in the watch list. These performance bugs were for general clauses, ternary clause propagation did not miss propagations (and don't use blocked literals), but fixing these issues for general clauses appear to have made ternary clause optimization irrelevant based on what was measured. * Update: Missing data-structures (still not compiling) * Nearly compiling * Some missing arguments * Polishing * Only conflicts/propagations/justifications are missing for making it compile * Added propagation (justifications for them are still missing) * Use the right deallocation * Use Z3's memory allocation system * Ported "seen" * Polishing * Added 64-bit "1" counting * More polishing * minor fixes - ensure mk_extract performs simplification to distribute over extract and removing extract if the range is the entire bit-vector - ensure bool_rewriter simplifeis disjunctions when applicable. * adding simplifiers layer simplifiers layer is a common substrate for global non-incremental and incremental processing. The first two layers are new, but others are to be ported form tactics. - bv::slice - rewrites equations to cut-dice-slice bit-vector extractions until they align. It creates opportunities for rewriting portions of bit-vectors to common sub-expressions, including values. - euf::completion - generalizes the KB simplifcation from asserted formulas to use the E-graph to establish a global and order-independent canonization. The interface dependent_expr_simplifier is amenable to forming tactics. Plugins for asserted-formulas is also possible but not yet realized. * Create bv_slice_tactic.cpp missing file * adding virtual destructor Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Added 64-bit "1" counting (#6434) * Memory leak in .NET user-propagator The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically * Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation * Added 64-bit "1" counting * remove incorrect assertion Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Added limit to "visit" to allow detecting multiple visits (#6435) * Memory leak in .NET user-propagator The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically * Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation * Added limit to "visit" to allow detecting multiple visits * Putting visit in a separate class (Reason: We will probably need two of them in the sat::solver) * Bugfix * init solve_eqs * working on solve_eqs * Update .gitignore * wip - converting the equation solver as a simplifier * make visited_helper independent of literals re-introduce shorthands in sat::solver for visited and have them convert literals to unsigned. * build fix * move model and proof converters to self-contained module * Create solve_eqs2_tactic.h * add converters module to python build * move tactic_params to params * move more converters * move horn_subsume_model_converter to ast/converters * add initial stubs for model reconstruction trail * fixing build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fixes #6439 #6436 * It's compiling (However, two important functions are commented out) Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>

zhendongsu · 2022-11-12T17:11:15Z

Refutation unsoundness:

[536] % z3release small.smt2 
sat
[537] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 
unsat
[538] % cat small.smt2 
(set-option :sat.prob_search true)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Bool)
(assert (or d (= 0 (+ b (* b c)))))
(assert (or (= 0 (+ 1 (* b c))) (and (= b 0) (> a 0) (= a 0))))
(check-sat-using (then nra qfnra-nlsat))

zhendongsu · 2022-11-13T09:56:37Z

Related to #6429 (comment):

[530] % z3debug small.smt2 
unsat
[531] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2 
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1195
m_columns_with_changed_bounds.empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[532] % cat small.smt2 
(set-option :smt.arith.ignore_int true)
(declare-fun f (Int Int) Int)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (= (* b (+ 1 (* 2 b))) (+ 1 (f (f a 0) (f a 0)))))
(assert (forall ((c Int)) (<= c 0)))
(check-sat)

zhendongsu · 2022-11-13T13:13:54Z

Another related instance:

[556] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1195
m_columns_with_changed_bounds.empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[557] % cat small.smt2
(set-option :smt.arith.ignore_int true)
(define-fun t ((c Int) (d Int) (a Int)) Int (mod (div a 0) 2))
(define-fun e ((a Int) (b Int)) Int (ite (or (= b 0)) 1 0))
(define-fun f ((c Int) (k Int)) Bool (<= k 0))
(define-fun g ((c Int)) Bool (forall ((b Int)) (= (and (f c b)) (= 0 (e 0 (t c 0 b))))))
(define-fun h ((c Int)) Bool (g c))
(define-fun i ((c Int)) Bool (h c))
(assert (forall ((j Int) (c Int)) (= (and (i c)) (= j 0))))
(check-sat-using bv)

zhendongsu · 2022-11-14T19:59:30Z

[525] % z3debug small.smt2 
sat
[526] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2 
ASSERTION VIOLATION
File: ../src/tactic/bv/bit_blaster_model_converter.cpp
Line: 151
bit_val
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[527] % cat small.smt2 
(set-option :sat.prob_search true)
(declare-fun I () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun Y () Float32)
(assert (distinct (_ bv0 32) (ite (fp.eq Y ((_ to_fp 8 24) (select I (_ bv0 32)))) (_ bv1 32) (_ bv0 32))))
(check-sat-using (then qfufbv_ackr bit-blast auflira))

zhendongsu · 2022-11-16T21:28:08Z

[578] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
(- (a 0) (a e!0)) := 1
(a c!3) := 0
(- (a 0) (a e!0)) -> ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 168
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[579] % cat small.smt2
(set-option :smt.arith.ignore_int true)
(declare-fun a (Int) Int)
(assert (= 1 (a 0)))
(assert (= 2 (a 1)))
(assert (forall ((c Int) (d Int)) (or (>= c d) (< (a c) (a d)))))
(assert (exists ((e Int)) (<= 0 (exists ((b Int)) (not (= (mod b 2) (a e)))))))
(check-sat)

zhendongsu · 2022-11-16T21:29:28Z

[534] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 16 80: (= 0.0 (select (select c d!2) x!1)) false
(sat
...
[535] % cat small.smt2
(set-option :smt.ematching false)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () (Array Int (Array Int Real)))
(assert (or false (and b (not (distinct (forall ((t Int)) false) (and a (forall ((x Int)) (and a (forall ((d Int)) (or (< d 0) (> d 1) (= 0 (select (select c d) x))))))))))))
(check-sat)

zhendongsu · 2022-11-16T22:31:42Z

[570] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 415
UNEXPECTED CODE WAS REACHED.
Z3 4.12.0.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] % cat small.smt2 
(set-option :rewriter.mul2concat true)
(set-option :rewriter.local_ctx true)
(declare-fun I () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (distinct (_ bv0 1) (bvnot ((_ extract 32 32) (bvadd ((_
  zero_extend 1) (select (store (store (store (store I (_ bv0 32) (_
  bv0 32)) (_ bv0 32) (_ bv0 32)) (_ bv1 32) (_ bv0 32)) (bvadd
  (select (store (store I (_ bv0 32) (_ bv0 32)) (_ bv0 32) (_ bv0
  32)) (_ bv1 32)) (_ bv0 32)) (_ bv4294967295 32)) (_ bv2 32))) ((_
  zero_extend 1) (select (store (store (store (store I (_ bv0 32) (_
  bv0 32)) (_ bv0 32) (_ bv0 32)) (_ bv1 32) (_ bv0 32)) (bvadd
  (select (store (store I (_ bv0 32) (_ bv0 32)) (_ bv0 32) (_ bv0
  32)) (_ bv1 32)) (_ bv0 32)) (_ bv4294967295 32)) (_ bv2 32))))))))
(push)
(check-sat)

zhendongsu · 2022-11-16T22:40:44Z

Another related instance:

[515] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 415
UNEXPECTED CODE WAS REACHED.
Z3 4.12.0.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[516] % cat small.smt2 
(set-option :rewriter.local_ctx true)
(declare-fun D () Float32)
(assert (= (_ bv0 1) (ite (fp.gt (fp.add roundTowardPositive D (_ +zero 8 24)) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23))) (_ bv1 1) (_ bv0 1))))
(check-sat)

zhendongsu · 2022-11-18T18:26:47Z

[519] % z3debug small.smt2 
unsat
[520] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2 
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 479
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[521] % cat small.smt2 
(assert (forall ((a Int) (b Int)) (distinct 0 (mod (+ a (mod b 3)) 2))))
(check-sat)

zhendongsu · 2022-11-19T09:07:43Z

[540] % z3san tactic.default_tactic=smt sat.euf=true small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==31590==ERROR: AddressSanitizer: stack-overflow on address 0x7fff62ba4f50 (pc 0x560700772cca bp 0x7fff62ba50a0 sp 0x7fff62ba4f20 T0)
    #0 0x560700772cc9 in smt::context::internalize_theory_atom(app*, bool) ../src/smt/smt_internalizer.cpp:492
    #1 0x560700780ccc in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:435
    #2 0x560700781269 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:375
    #3 0x56070077f896 in smt::context::internalize_formula_core(app*, bool) ../src/smt/smt_internalizer.cpp:643
    #4 0x560700780ac1 in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:440
    #5 0x560700781269 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:375
...
SUMMARY: AddressSanitizer: stack-overflow ../src/smt/smt_internalizer.cpp:492 in smt::context::internalize_theory_atom(app*, bool)
==31590==ABORTING
[541] % cat small.smt2
(set-option :rewriter.local_ctx true)
(declare-fun c () Float64)
(declare-fun b () Float64)
(declare-fun d () Float64)
(assert (= d (fp #b0 #b11100111110 #b0111110000100110010110110111011001001000001011001101)))
(assert (= (fp.sub roundTowardZero c b) d))
(check-sat-using (then dom-simplify purify-arith ctx-solver-simplify))

zhendongsu · 2022-11-19T23:45:15Z

Refutation unsoundness:

[554] % z3release model_validate=true small.smt2 
sat
[555] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
unsat
[556] % cat small.smt2 
(set-option :sat.prob_search true)
(declare-fun a () Bool)
(declare-fun b () Int)
(declare-fun c () Bool)
(assert (= b (ite (< (ite (> 4 (+ 1 (ite c (ite a 0 (+ 1 1 1)) (- (ite a 0 (+ 1 1 1)) 1)))) b 0) 0) 1 0)))
(check-sat-using (then lira ufbv qfnia auflira qfidl))

zhendongsu · 2022-11-20T08:50:53Z

[612] % z3-4.11.2 tactic.default_tactic=smt sat.euf=true small.smt2
unknown
[613] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/ast/rewriter/rewriter_def.h
Line: 226
UNEXPECTED CODE WAS REACHED.
Z3 4.12.0.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[614] % cat small.smt2
(set-option :smt.phase_selection 5)
(set-option :rewriter.local_ctx true)
(set-option :smt.threads 2)
(declare-fun a () Float32)
(assert (distinct a (_ NaN 8 24)))
(assert (fp.geq a (_ +zero 8 24)))
(assert (fp.leq a (fp #b0 #x9f #b00000000000000000000000)))
(assert (not (bvult ((_ fp.to_ubv 32) RTZ a) #x00000064)))
(check-sat-using (then simplify ctx-solver-simplify))

zhendongsu · 2022-11-20T22:47:56Z

[581] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Failed to validate 7 90: (= 1 (select (select b c!0) 0)) true
(sat
...
[582] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () (Array Int (Array Int Int)))
(assert (or (exists ((c Int)) (> c (- a))) (exists ((d Int) (e Int)) (distinct (= 1 (select (select b d) 0)) (distinct (< e 1) (>= d 0 e))))))
(check-sat)

zhendongsu · 2022-11-23T08:01:35Z

[545] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/ast/euf/euf_egraph.cpp
Line: 169
n->value() == l_false
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[546] % cat small.smt2
(declare-fun a () Real)
(assert (or true (or (or (not (distinct 0 a)) (not (= a 0))))))
(check-sat)

zhendongsu · 2022-11-23T08:04:41Z

[538] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 479
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[539] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/ast/euf/euf_egraph.cpp
Line: 109
!find(f)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[540] % cat small.smt2 
(assert (= 0 (ite (or false) 1 0)))
(check-sat)

zhendongsu · 2022-11-24T08:32:11Z

[534] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault
[535] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault
[536] % z3san tactic.default_tactic=smt sat.euf=true small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==13421==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000038 (pc 0x5567c381de33 bp 0x7ffd3e5d7620 sp 0x7ffd3e5d6df0 T0)
==13421==The signal is caused by a READ memory access.
==13421==Hint: address points to the zero page.
    #0 0x5567c381de32 in euf::egraph::merge(euf::enode*, euf::enode*, euf::justification) ../src/ast/euf/euf_egraph.cpp:447
    #1 0x5567c0780dea in euf::egraph::merge(euf::enode*, euf::enode*, void*) ../src/ast/euf/euf_egraph.h:261
    #2 0x5567c0780dea in euf::solver::propagate_literals() ../src/sat/smt/euf_solver.cpp:477
    #3 0x5567c0782216 in euf::solver::unit_propagate() ../src/sat/smt/euf_solver.cpp:417
    #4 0x5567c35ebc1e in sat::solver::propagate_core(bool) ../src/sat/sat_solver.cpp:974
    #5 0x5567c3600bb1 in sat::solver::propagate(bool) ../src/sat/sat_solver.cpp:986
    #6 0x5567c3600bb1 in sat::solver::basic_search() ../src/sat/sat_solver.cpp:1685
    #7 0x5567c36016c1 in sat::solver::bounded_search() ../src/sat/sat_solver.cpp:1678
    #8 0x5567c3602759 in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1288
    #9 0x5567c076d501 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:73
    #10 0x5567c0771d0b in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:221
    #11 0x5567c256af3c in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1032
    #12 0x5567c25785fa in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #13 0x5567c25785fa in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #14 0x5567c25785fa in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #15 0x5567c253fa04 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:165
    #16 0x5567c2541424 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:185
    #17 0x5567c22d6e32 in check_sat_using_tactic_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:216
    #18 0x5567c229def8 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2910
    #19 0x5567c22a25cc in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3016
    #20 0x5567c22a25cc in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3166
    #21 0x5567c22578a5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3217
    #22 0x5567bf2f6351 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:144
    #23 0x5567bf2ca191 in main ../src/shell/main.cpp:381
    #24 0x7f16792e0c86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86)
    #25 0x5567bf2d70f9 in _start (/local/suz-local/software/z3san/build-11232022183517-4ac5e51/z3+0x2060f9)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/euf/euf_egraph.cpp:447 in euf::egraph::merge(euf::enode*, euf::enode*, euf::justification)
==13421==ABORTING
[537] % 
[537] % cat small.smt2
(set-option :rewriter.expand_nested_stores true)
(declare-const a (_ BitVec 1))
(declare-const b (Array (_ BitVec 32) (_ BitVec 8)))
(declare-const c (_ BitVec 1))
(declare-const d (Array (_ BitVec 32) (_ BitVec 8)))
(assert (= c (ite (= b (store (store (store d (_ bv0 32) (_ bv0 8)) ((_ zero_extend 16) ((_ zero_extend 14) ((_ zero_extend 1) a))) (_ bv1 8)) (_ bv0 32) (_ bv0 8))) (_ bv1 1) (_ bv0 1))))
(check-sat-using (then qfnia qfidl ufbv))

zhendongsu · 2023-01-04T15:36:08Z

Another instance of the assertion violation at ../src/math/lp/lar_solver.cpp, Line: 1195:

[569] % z3debug small.smt2
sat
[570] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1195
m_columns_with_changed_bounds.empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[571] % cat small.smt2
(set-option :smt.arith.ignore_int true)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (or (forall ((d Int) (g Int)) (distinct c (+ (* 4 d) g))) (forall ((e Int)) (= b 0)) (forall ((f Int) (h Int)) (= (- h f) a))))
(check-sat)

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

NikolajBjorner · 2023-01-05T17:25:35Z

moved remaining to #6523

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

NikolajBjorner added a commit that referenced this issue Oct 29, 2022

#6429

0da0fa2

NikolajBjorner added a commit that referenced this issue Nov 23, 2022

#6429

f87e187

NikolajBjorner added a commit that referenced this issue Nov 23, 2022

#6429

4ac5e51

NikolajBjorner added a commit that referenced this issue Jan 4, 2023

update ignore-int handling #6429

aa080a6

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

NikolajBjorner added a commit that referenced this issue Jan 4, 2023

#6429 fixes

ef10119

NikolajBjorner added a commit that referenced this issue Jan 4, 2023

#6429

e009915

NikolajBjorner added a commit that referenced this issue Jan 4, 2023

#6429

81ce57b

NikolajBjorner closed this as completed Jan 5, 2023

hgvk94 pushed a commit to hgvk94/z3 that referenced this issue Mar 27, 2023

Z3Prover#6429

c4e3ec1

hgvk94 pushed a commit to hgvk94/z3 that referenced this issue Mar 27, 2023

Z3Prover#6429

37a4242

hgvk94 pushed a commit to hgvk94/z3 that referenced this issue Mar 27, 2023

update ignore-int handling Z3Prover#6429

bb4f250

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

hgvk94 pushed a commit to hgvk94/z3 that referenced this issue Mar 27, 2023

Z3Prover#6429 fixes

081c413

hgvk94 pushed a commit to hgvk94/z3 that referenced this issue Mar 27, 2023

Z3Prover#6429

fd4ef88

hgvk94 pushed a commit to hgvk94/z3 that referenced this issue Mar 27, 2023

Z3Prover#6429

3ef9653

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[consolidated] issues with new core #6429

[consolidated] issues with new core #6429

zhendongsu commented Oct 29, 2022

zhendongsu commented Oct 30, 2022

zhendongsu commented Oct 30, 2022

zhendongsu commented Oct 30, 2022

zhendongsu commented Oct 31, 2022

zhendongsu commented Nov 2, 2022

zhendongsu commented Nov 3, 2022

zhendongsu commented Nov 12, 2022

zhendongsu commented Nov 13, 2022

zhendongsu commented Nov 13, 2022

zhendongsu commented Nov 14, 2022

zhendongsu commented Nov 16, 2022

zhendongsu commented Nov 16, 2022

zhendongsu commented Nov 16, 2022

zhendongsu commented Nov 16, 2022

zhendongsu commented Nov 18, 2022

zhendongsu commented Nov 19, 2022

zhendongsu commented Nov 19, 2022

zhendongsu commented Nov 20, 2022

zhendongsu commented Nov 20, 2022

zhendongsu commented Nov 23, 2022

zhendongsu commented Nov 23, 2022

zhendongsu commented Nov 24, 2022

zhendongsu commented Jan 4, 2023

NikolajBjorner commented Jan 5, 2023

[consolidated] issues with new core #6429

[consolidated] issues with new core #6429

Comments

zhendongsu commented Oct 29, 2022

zhendongsu commented Oct 30, 2022

zhendongsu commented Oct 30, 2022

zhendongsu commented Oct 30, 2022

zhendongsu commented Oct 31, 2022

zhendongsu commented Nov 2, 2022

zhendongsu commented Nov 3, 2022

zhendongsu commented Nov 12, 2022

zhendongsu commented Nov 13, 2022

zhendongsu commented Nov 13, 2022

zhendongsu commented Nov 14, 2022

zhendongsu commented Nov 16, 2022

zhendongsu commented Nov 16, 2022

zhendongsu commented Nov 16, 2022

zhendongsu commented Nov 16, 2022

zhendongsu commented Nov 18, 2022

zhendongsu commented Nov 19, 2022

zhendongsu commented Nov 19, 2022

zhendongsu commented Nov 20, 2022

zhendongsu commented Nov 20, 2022

zhendongsu commented Nov 23, 2022

zhendongsu commented Nov 23, 2022

zhendongsu commented Nov 24, 2022

zhendongsu commented Jan 4, 2023

NikolajBjorner commented Jan 5, 2023