[consolidated] new core #7027

NikolajBjorner · 2023-11-30T16:28:42Z

[511] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
Failed to validate 60 741: (= (o (a #186)) (o (a #668))) false
(sat
...
[512] % cat small.smt2 
(declare-datatypes ((a 0)) (((a (o (Array (_ BitVec 2) (_ BitVec 2)))))))
(declare-fun r ((_ BitVec 2) a (_ BitVec 2)) Bool)
(assert (forall ((a a) (s (_ BitVec 2))) (= (bvsge s (_ bv0 2)) (r s a (_ bv0 2)))))
(check-sat)

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

NikolajBjorner · 2023-11-30T16:29:34Z

$ cat small.smt2 
(declare-fun b (Real Real) Real)
(declare-fun u (Real Real) (Array Real Real))
(assert (forall ((v Real) (r Real)) (= v (select (u v (b 0.0 0.0)) r))))
(check-sat)
$ z3 tactic.default_tactic=smt sat.euf=true rewriter.eq2ineq=true small.smt2
(u (b 0.0 0.0) (b 0.0 0.0)) := ((as const (Array Real Real)) 0.0)
(u v!2 (b 0.0 0.0)) := ((as const (Array Real Real)) (- 1.0))
(u (b 0.0 0.0) (b 0.0 0.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

This one doesn't hit the assert at this point

NikolajBjorner · 2023-11-30T16:31:46Z

[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))

I am going to punt on looking into this one. It is total abuse of features to mix FP with nra, qe.

merlinsun · 2023-12-02T06:30:51Z

$ cat small.smt2 
(declare-const x (Array Bool Int))
(declare-const x2 (Array Bool Int))
(declare-fun v () (Array Bool Int))
(assert (forall ((a Bool)) (or (distinct x x2 v) (> 0 (select x2 a)))))
(check-sat-using qe2)
$ z3 tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 482
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

merlinsun · 2023-12-02T07:03:51Z

$ cat small.smt2 
(set-option :tactic.default_tactic smt)
(set-option :sat.euf true)
(set-option :rewriter.arith_lhs true)
(set-option :model_validate true)
(declare-fun va () Real)
(declare-fun r () Real)
(declare-fun r2 () Real)
(declare-fun a () Real)
(declare-fun v () Real)
(push 3)
(assert (or (and (= 0.0 va) (= va 1.0)) (= 3 (/ 1.0 (+ r 6 (/ 0.6 r)))) (and (= 0.0 r2) (= r2 va) (= a 0.0))))
(assert (forall ((ar Real)) (or (distinct 0 v) (= 0.0 (* ar (to_real (to_int va)))))))
(check-sat)
$ z3 small.smt2 
sat
failed to verify: (let ((a!1 (= (to_real 3) (/ 1.0 (+ r (to_real 6) (/ (/ 3.0 5.0) r))))))
  (or (and (= 0.0 va) (= va 1.0)) a!1 (and (= 0.0 r2) (= r2 va) (= a 0.0))))
evaluated to false
...

zhendongsu · 2023-12-02T19:59:49Z

Refutation unsoundness issue:

[562] % z3release small.smt2
sat
sat
[563] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
sat
unsat
[564] % cat small.smt2
(declare-fun a () Bool)
(declare-fun b (Int) Int)
(declare-fun c (Int) Int)
(declare-fun d (Int) Int)
(declare-fun e (Int) Int)
(declare-fun f (Int) Int)
(declare-fun g () Int)
(declare-fun h (Int) Int)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun k () Int)
(declare-fun l () Int)
(declare-fun p (Int) Int)
(declare-fun q () Int)
(check-sat)
(assert (let ((m i) (n l) (o (h 1))) (and (distinct 0 (f 0)) (distinct
  0 (b (c 0))) (distinct 0 (e (c 0))) (distinct 0 (e 1)) (= (c 0) (b
  g)) (= 1 (b q)) (= l (b i)) (= 0 (b j)) (distinct l (b 0)) (= i (b
  1)) (= (b l) (f 1)0 (p 0)) (= l (d 0)) (= 0 (d j)) (= 1 (d l)) (= 0
  (e 0)) (= (h 1) k) (or (= k (h i)) (= 0 (h i))) (= (b k)0 (f g)) (=
  i (d k)) (= 0 (e q)) (distinct g (c 0)) (distinct j k) (distinct i
  (c 0)) (distinct j 1) a (<= 0 g) (< g 8) (< 0 q 8) (<= 0 i) (< i 8)
  (<= 0 j) (< j 8) (<= 0 k) (< k 8) (<= 0 (c 0)) (< (c 0) 8) (< 0 l
  8))))
(check-sat)

zhendongsu · 2023-12-02T20:01:50Z

[579] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Failed to validate 2 9: (is c (h x)) false
(sat
...
[580] % cat small.smt2 
(declare-datatypes ((n 0) (l 0) (t 0)) (((z)) ((n) (c (a t))) ((n (h l)) (l (d n)))))
(declare-fun x () t)
(assert (= (d (a (h x))) (d (ite ((_ is c) (h x)) (a (h x)) x))))
(check-sat)

zhendongsu · 2023-12-02T20:03:25Z

Refutation unsoundness:

[594] % z3release small.smt2 
sat
[595] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
unsat
[596] % cat small.smt2 
(declare-fun A () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= (_ bv0 1) (ite (= (_ bv0 32) ((_ zero_extend 31) ((_ extract 0 0) (select A (_ bv1 32))))) (_ bv1 1) (_ bv0 1))))
(assert (bvsle (_ bv0 32) (select (store (store (store A (_ bv0 32) (_ bv0 32)) (select (store (store A (_ bv0 32) (_ bv0 32)) (select (store A (_ bv0 32) (_ bv0 32)) (_ bv0 32)) (_ bv0 32)) (_ bv0 32)) (_ bv0 32)) (select (store (store A (_ bv0 32) (_ bv0 32)) (_ bv1 32) (_ bv0 32)) (_ bv0 32)) (_ bv0 32)) (_ bv0 32))))
(check-sat)

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

zhendongsu · 2023-12-02T21:14:54Z

[512] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 477
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[513] % cat small.smt2 
(declare-fun a (Int Int) Int)
(declare-fun b (Int Int Int) (Array Int (Array Int Int)))
(assert (forall ((c Int) (d Int) (e Int) (f Int) (g Int) (h Int) (i Int)) (= i (select (select (b 0 (a 0 0) (a 0 h)) d) e))))
(check-sat)

zhendongsu · 2023-12-02T21:20:38Z

[546] % z3release small.smt2 
sat
sat
sat
[547] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 
sat
sat
unsat
[548] % cat small.smt2 
(declare-fun a () Real)
(declare-fun b () Real)
(assert (= b (* a (+ a b))))
(check-sat)
(assert (distinct 0.0 (+ a b)))
(check-sat)
(check-sat)

zhendongsu · 2023-12-02T21:21:49Z

[555] % z3release small.smt2 
sat
[556] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 
unsat
[557] % cat small.smt2 
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (distinct (bvsmod (_ bv0 1) (bvlshr (_ bv0 1) (bvadd (_ bv1 1) (ite (= (_ bv0 1) (ite (distinct b (store (store (store a (bvadd (_ bv1 32)) (_ bv1 8)) (bvsmod (_ bv0 32) (_ bv0 32)) (_ bv0 8)) (_ bv0 32) (_ bv0 8))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))))))
(check-sat)

zhendongsu · 2023-12-03T09:15:50Z

[592] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Failed to validate 4 16: (< (* b (+ a 1.0)) 0.0) false
(sat
...
[593] % cat small.smt2 
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (> 0.0 b))
(assert (>= 0.0 a))
(assert (distinct 0.0 (* a c)))
(assert (< (* b (+ a 1.0)) 0.0))
(check-sat)

fix lossy function declaration inclusion functionality exposed when fixing a bug for incomplete model generation.

exposed by #7027, but generally missing. It is less likely to be exposed if input is normalized by distributing multiplication over addition.

zhendongsu · 2023-12-04T20:43:40Z

[581] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
num-conflicts: 198
ASSERTION VIOLATION
File: ../src/sat/sat_solver.cpp
Line: 2564
Failed to verify: idx > 0

Z3 4.12.3.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[582] % cat small.smt2
(declare-fun a () Bool)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(assert a)
(assert (< e 2))
(assert (or (= h 0) (distinct (= 0 b)) (and (< (- e) 0) (= (+ f (- f)) (- 1 (ite false (ite false 0 (- g (+ d (- e (+ (- 10) (- 2 (* f 4096))))))) (- (* c 16) (+ g 0 d))))))))
(check-sat)

zhendongsu · 2024-01-21T18:57:57Z

Refutation unsoundness:

[545] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
sat
[546] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(assert (< 0 (+ b a (* b (- 1)))))
(assert (< (+ d e (* 2 i) (* h (- 1))) 1))
(assert (< (+ c i) 0))
(assert (< (+ 2 (* i (- 1))) 1 (- (+ e f g) (* c (- 2)))))
(assert (< (* h (- 1)) 1))
(assert (< c 0))
(assert (< (+ (* i (- 1)) d f) 0))
(assert (< (+ e d) 1))
(assert (< (+ g (* 2 h) (* f (- 2))) 1))
(check-sat)

(reset)

(define-fun a () Int 1)
(define-fun b () Int 0)
(define-fun c () Int (- 3))
(define-fun d () Int (- 3))
(define-fun e () Int 2)
(define-fun f () Int 4)
(define-fun g () Int 2)
(define-fun h () Int 3)
(define-fun i () Int 2)
(assert (< 0 (+ b a (* b (- 1)))))
(assert (< (+ d e (* 2 i) (* h (- 1))) 1))
(assert (< (+ c i) 0))
(assert (< (+ 2 (* i (- 1))) 1 (- (+ e f g) (* c (- 2)))))
(assert (< (* h (- 1)) 1))
(assert (< c 0))
(assert (< (+ (* i (- 1)) d f) 0))
(assert (< (+ e d) 1))
(assert (< (+ g (* 2 h) (* f (- 2))) 1))
(check-sat)

merlinsun · 2024-02-21T13:59:29Z

$ cat small.smt2 
(declare-fun var2647 () Real)
(declare-fun ar7 () Real)
(assert (forall ((v Real)) (distinct (= v 0) (= 0 (+ var2647 ar7)))))
(check-sat-using qsat)
$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1534
t->is_empty() == false
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

muchang · 2024-03-10T12:42:12Z

Here is a simpler trigger for the above assertion violation:

$ cat small.smt2 
(declare-fun a () Real) 
(assert (not (>= (* (* a (+ 5 a))) 0))) 
(check-sat)   
$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1534
t->is_empty() == false
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

version: 7bbe3fb

NB: The code doesn't exist any longer.

Update: It has been fixed in the latest commit.

z3/src/math/lp/lar_solver.cpp

Line 1534 in 7bbe3fb

SASSERT (!t->is_empty());

zhendongsu · 2024-03-14T12:02:25Z

Hang on a small formula:

[507] % timeout -s 9 30 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[508] % time z3-4.11.2 tactic.default_tactic=smt sat.euf=true small.smt2 
sat

real	0m0.343s
user	0m0.124s
sys	0m0.016s
[509] % cat small.smt2 
(declare-const a Int)
(assert (= (mod (* a a) a) 1))
(check-sat)

zhendongsu · 2024-03-17T17:39:33Z

Another related instance:

[639] % time z3release small.smt2 
sat

real    0m0.102s
user    0m0.015s
sys     0m0.027s
[640] % timeout -s 9 30 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[641] % cat small.smt2 
(declare-const a Int)
(assert (> a (div (* a (abs a)) 1)))
(check-sat)

zhendongsu · 2024-03-17T17:40:05Z

[628] % time z3release small.smt2 
sat

real    0m0.111s
user    0m0.052s
sys     0m0.004s
[629] % timeout -s 9 30 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[630] % cat small.smt2 
(declare-const a Int)
(declare-const b Int)
(assert (> 0 (- (* (mod b a) a) a)))
(check-sat)

zhendongsu · 2024-03-19T17:03:25Z

[568] % time z3release small.smt2 
sat

real	0m0.607s
user	0m0.399s
sys	0m0.208s
[569] % timeout -s 9 30 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[570] % cat small.smt2 
(declare-const a (_ BitVec 64))
(assert (bvult a (bvurem #x1111111111111111 (bvlshr a #x0000000000000000))))
(check-sat)

zhendongsu · 2024-03-20T18:55:18Z

[520] % time z3release small.smt2 
sat

real	0m0.067s
user	0m0.045s
sys	0m0.020s
[521] % timeout -s 9 60 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[522] % cat small.smt2 
(declare-const a (_ BitVec 64))
(assert (= 0 (bv2nat a)))
(check-sat)

zhendongsu · 2024-03-25T12:43:30Z

[592] % time z3release small.smt2 
sat

real	0m0.124s
user	0m0.042s
sys	0m0.012s
[593] % time z3-4.11.2 tactic.default_tactic=smt sat.euf=true small.smt2 
sat

real	0m0.056s
user	0m0.013s
sys	0m0.010s
[594] % timeout -s 9 60 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[595] % cat small.smt2 
(declare-const a Int)
(declare-const b Int)
(assert (>= (* b (- b (mod a b))) 2))
(check-sat)

zhendongsu · 2024-03-25T13:50:46Z

[558] % time z3release small.smt2 
sat

real	0m0.062s
user	0m0.022s
sys	0m0.014s
[559] % time z3-4.11.2 tactic.default_tactic=smt sat.euf=true small.smt2 
sat

real	0m0.030s
user	0m0.004s
sys	0m0.018s
[560] % timeout -s 9 60 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[561] % cat small.smt2 
(declare-const a Int)
(declare-const b Int)
(assert (< 2 a (* a b)))
(check-sat)

zhendongsu · 2024-03-27T08:25:33Z

[528] % time z3release small.smt2 
sat

real	0m0.104s
user	0m0.017s
sys	0m0.017s
[529] % time z3-4.11.2 tactic.default_tactic=smt sat.euf=true small.smt2 
sat

real	0m0.346s
user	0m0.156s
sys	0m0.017s
[530] % timeout -s 9 60 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[531] % cat small.smt2 
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(assert (< (mod a (* b c)) (mod a b)))
(check-sat)

zhendongsu · 2024-03-27T08:54:24Z

[543] % time z3release small.smt2 
unsat

real    0m0.140s
user    0m0.040s
sys     0m0.016s
[544] % time z3-4.11.2 tactic.default_tactic=smt sat.euf=true small.smt2 
unsat

real    0m0.050s
user    0m0.005s
sys     0m0.020s
[545] % timeout -s 9 60 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[546] % cat small.smt2 
(declare-const a Int)
(declare-const b Int)
(assert (= (* (mod (+ a a) b) b) 2))
(check-sat)

zhendongsu · 2024-03-27T08:58:55Z

[662] % time z3release small.smt2 
sat

real	0m0.100s
user	0m0.016s
sys	0m0.024s
[663] % time z3-4.11.2 tactic.default_tactic=smt sat.euf=true small.smt2 
sat

real	0m0.047s
user	0m0.004s
sys	0m0.019s
[664] % timeout -s 9 60 z3release tactic.default_tactic=smt sat.euf=true small.smt2
Killed
[666] % cat small.smt2 
(declare-const a Int)
(declare-const b Int)
(assert (<= 2 (* (- (* a a) a) b)))
(check-sat)

merlinsun · 2024-04-24T08:47:04Z

$ cat delta.out.smt2
(declare-fun var1307 () (Array Bool Int))
(assert (forall ((var1306 (Array Bool Int)) (var107 Int)) (xor (= 0 (select (store var1306 (= var1306 var1307) 0) false)) (< var107 2))))
(check-sat-using (then qe2 ctx-solver-simplify))
$ z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/qe/qe_mbp.cpp
Line: 404
Failed to verify: !model.is_false(f)

merlinsun · 2024-05-05T02:35:00Z

Refutation unsoundness issue:

$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
unsat
$ z3 small.smt2
sat
$ cat small.smt2
(declare-fun v () (Array Bool Int))
(declare-fun a () Bool)
(declare-fun va () Bool)
(assert (forall ((R Real)) (= (store (store v false 0) a 3) (store (store v va 1) true 0))))
(check-sat)

merlinsun · 2024-05-05T03:00:59Z

$ cat small.smt2 
(declare-const x Bool)
(declare-fun b (Int Int Real) (Array Int (Array Int Real)))
(declare-fun b (Int Int) Int)
(declare-fun v () Bool)
(declare-fun a () Int)
(declare-fun r () (Array Bool (Array Real Real)))
(declare-fun r3 () Real)
(assert (or v false (< 0.0 0.0)))
(assert (forall ((va Real)) (xor (= a 0) (= va (select (select (b (b 0 0) (b 0 0) va) 0) 0)) x (= 1.0 (* r3 (select (select r true) 0.0))))))
(check-sat-using sat)
$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
(b (b 0 0) (b 0 0) (select (select r true) 0.0)) := (let ((a!1 (store ((as const (Array Int (Array Int Real)))
...
  (store a!1 0 ((as const (Array Int Real)) (/ 1.0 3579.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

merlinsun · 2024-05-08T06:53:06Z

Another case potentially relevant to #7027 (comment)

$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
unsat
$ z3 small.smt2 
sat
$ cat small.smt2 
(declare-fun v () (Array Bool Int))
(declare-fun a () Bool)
(assert (exists ((r Bool)) (= (store (store v false 0) r 3) (store (store v a 1) true 0))))
(check-sat)

merlinsun · 2024-05-18T12:56:25Z

$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/pb_solver.cpp
Line: 3467
Failed to verify: this == sat::constraint_base::to_extension(index)

$ cat small.smt2 
(declare-fun ar4 () Int)
(declare-fun r41 () Int)
(declare-fun r411 () Int)
(declare-fun r412 () Int)
(declare-fun r413 () Int)
(declare-fun r () Int)
(declare-fun r4128 () Int)
(declare-fun r4119 () Int)
(declare-fun r8 () Int)
(declare-fun r4126 () Int)
(declare-fun ar41 () Int)
(declare-fun r4124 () Int)
(declare-fun r5 () Int)
(declare-fun r4125 () Int)
(declare-fun var41 () Int)
(declare-fun ar412 () Int)
(declare-fun r45 () Int)
(declare-fun va () Int)
(declare-fun a () Int)
(declare-fun var () Int)
(declare-fun r6 () Int)
(declare-fun ar5 () Int)
(declare-fun r4120 () Int)
(declare-fun r58 () Int)
(declare-fun ar () Real)
(declare-fun r4127 () Int)
(declare-fun r4121 () Int)
(declare-fun r4 () Int)
(declare-fun var4 () Int)
(declare-fun r46 () Int)
(declare-fun v () Int)
(assert (distinct 1 var ar5 r8 r6 v r5 a va r45 r var4 r58 ar r46 r4 0 r411 ar41 var41 r4119 r4120 r4121 ar4 r412 r4124 r4125 r4126 r4127 r4128 ar412 r413 r41))
(check-sat-using qe2)

wintered · 2024-08-17T20:05:40Z

Soundness Issue on simple Integer formula with mod

c1454dc

$z3release model_validate=true tactic.default_tactic=smt sat.euf=true bug.smt2
unsat
$z3release tactic.default_tactic=smt sat.euf=true bug.smt2                   
sat
$z3release model_validate=true bug.smt2 
sat
$cat bug.smt2 
(declare-const a Int)
(declare-const b Int)
(assert (or (<= (mod 1 a) a) (< b b)))
(check-sat)

NikolajBjorner mentioned this issue Nov 30, 2023

[consolidated] issues with new core #6523

Closed

NikolajBjorner added a commit that referenced this issue Dec 2, 2023

#7027

331507c

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

NikolajBjorner added a commit that referenced this issue Dec 3, 2023

#7027

362d299

NikolajBjorner added a commit that referenced this issue Dec 3, 2023

#7027

9cc2ce4

fix lossy function declaration inclusion functionality exposed when fixing a bug for incomplete model generation.

NikolajBjorner added a commit that referenced this issue Dec 3, 2023

fix cone of influence computation for terms with nested variables

f06e07a

exposed by #7027, but generally missing. It is less likely to be exposed if input is normalized by distributing multiplication over addition.

NikolajBjorner closed this as completed in be7856c Jan 23, 2024

NikolajBjorner reopened this Jan 23, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[consolidated] new core #7027

[consolidated] new core #7027

NikolajBjorner commented Nov 30, 2023 •

edited

Loading

NikolajBjorner commented Nov 30, 2023 •

edited

Loading

NikolajBjorner commented Nov 30, 2023 •

edited

Loading

merlinsun commented Dec 2, 2023

merlinsun commented Dec 2, 2023

zhendongsu commented Dec 2, 2023

zhendongsu commented Dec 2, 2023

zhendongsu commented Dec 2, 2023

zhendongsu commented Dec 2, 2023

zhendongsu commented Dec 2, 2023

zhendongsu commented Dec 2, 2023

zhendongsu commented Dec 3, 2023

zhendongsu commented Dec 4, 2023

zhendongsu commented Jan 21, 2024

merlinsun commented Feb 21, 2024

muchang commented Mar 10, 2024 •

edited

Loading

zhendongsu commented Mar 14, 2024

zhendongsu commented Mar 17, 2024

zhendongsu commented Mar 17, 2024

zhendongsu commented Mar 19, 2024

zhendongsu commented Mar 20, 2024

zhendongsu commented Mar 25, 2024

zhendongsu commented Mar 25, 2024

zhendongsu commented Mar 27, 2024

zhendongsu commented Mar 27, 2024

zhendongsu commented Mar 27, 2024

merlinsun commented Apr 24, 2024

merlinsun commented May 5, 2024

merlinsun commented May 5, 2024

merlinsun commented May 8, 2024

merlinsun commented May 18, 2024

wintered commented Aug 17, 2024

[consolidated] new core #7027

[consolidated] new core #7027

Comments

NikolajBjorner commented Nov 30, 2023 • edited Loading

NikolajBjorner commented Nov 30, 2023 • edited Loading

NikolajBjorner commented Nov 30, 2023 • edited Loading

merlinsun commented Dec 2, 2023

merlinsun commented Dec 2, 2023

zhendongsu commented Dec 2, 2023

zhendongsu commented Dec 2, 2023

zhendongsu commented Dec 2, 2023

zhendongsu commented Dec 2, 2023

zhendongsu commented Dec 2, 2023

zhendongsu commented Dec 2, 2023

zhendongsu commented Dec 3, 2023

zhendongsu commented Dec 4, 2023

zhendongsu commented Jan 21, 2024

merlinsun commented Feb 21, 2024

muchang commented Mar 10, 2024 • edited Loading

zhendongsu commented Mar 14, 2024

zhendongsu commented Mar 17, 2024

zhendongsu commented Mar 17, 2024

zhendongsu commented Mar 19, 2024

zhendongsu commented Mar 20, 2024

zhendongsu commented Mar 25, 2024

zhendongsu commented Mar 25, 2024

zhendongsu commented Mar 27, 2024

zhendongsu commented Mar 27, 2024

zhendongsu commented Mar 27, 2024

merlinsun commented Apr 24, 2024

merlinsun commented May 5, 2024

merlinsun commented May 5, 2024

merlinsun commented May 8, 2024

merlinsun commented May 18, 2024

wintered commented Aug 17, 2024

NikolajBjorner commented Nov 30, 2023 •

edited

Loading

NikolajBjorner commented Nov 30, 2023 •

edited

Loading

NikolajBjorner commented Nov 30, 2023 •

edited

Loading

muchang commented Mar 10, 2024 •

edited

Loading