[consolidated] issues in the new core #6116

zhendongsu · 2022-06-28T22:35:39Z

Refutation unsoundess:

[580] % z3release small.smt2
sat
[581] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
unsat
[582] % cat small.smt2
(declare-sort a 0)
(declare-sort b 0)
(declare-const c a)
(declare-fun counter (a b) Int)
(declare-fun d (a Int b) Int)
(declare-const j a)
(declare-const e b)
(declare-fun f (b) Int)
(declare-const k b)
(declare-const g a)
(assert (forall ((h b)) (and (=> (> (f h) 0) (= (counter j h) 0)) (> (f h) 0) (= (d g 0 h) 7) (forall ((i Int)) (=> (not (= i (counter j h))) (= 0 (d j i h)))))))
(assert (forall ((h b) (i Int)) (= (d c i h) (d g i h))))
(assert (not (forall ((i Int)) (= (d c i e) (d c i k)))))
(check-sat)

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

zhendongsu · 2022-06-28T22:49:46Z

Refutation unsoundness:

[594] % z3release small.smt2
sat
[595] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[596] % cat small.smt2
(define-fun c ((d Int) (a Int) (b Int)) Int (ite (= b 0) 0 (div a b)))
(define-fun e ((d Int) (f Int)) Int (- f))
(define-fun o ((d Int) (a Int) (b Int)) Bool (< (e d a) 0))
(define-fun g ((d Int) (a Int) (b Int)) Bool (= 0 0))
(define-fun h ((d Int) (f Int) (i Int) (k Int)) Bool (o d (c d f i) k))
(define-fun m ((d Int) (i Int) (k Int)) Bool (= (g d k 0) (o d (c d d i) k)))
(declare-fun d () Int)
(declare-fun i () Int)
(declare-fun k () Int)
(declare-fun j () Int)
(assert (h d j i k))
(assert (not (m d i k)))
(check-sat)

merlinsun · 2022-06-29T02:21:51Z

$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
unsat
$ z3 delta.smt2
sat
$ cat delta.smt2
(declare-fun v () Real)
(assert (forall ((a Real)) (= 0.0 (* v (mod 1 (to_int (/ 1.0 a)))))))
(assert (= 0.0 (/ 1 1.0 0.0)))
(check-sat)

merlinsun · 2022-06-29T02:33:11Z

$ z3 tactic.default_tactic=smt sat.euf=true delta2.smt2
unsat
$ z3 delta2.smt2
sat
$ cat delta2.smt2
(set-logic ALL)
(assert (= 0.0 (* 0.0 (div 1 (to_int 1.0)))))
(check-sat)

wintered · 2022-06-29T17:33:48Z

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

wintered · 2022-06-29T17:58:42Z

$z3release bug.smt2
sat
$z3release tactic.default_tactic=smt sat.euf=true bug.smt2
unsat
$cat bug.smt2 
(assert (> 0 (div 1 (- 1)))) 
(check-sat)

zhendongsu · 2022-06-30T12:11:15Z

Not sure whether this is of interest as it involves optimizations, but the formula is trivial:

[544] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 7 column 10: an invalid model was generated")
(
  (define-fun b () Real
    (- 1.0))
  (define-fun a () Real
    0.0)
  (define-fun c () Bool
    false)
)
[545] % cat small.smt2
(declare-const a Real)
(declare-const b Real)
(declare-const c Bool)
(assert (or c (= a b)))
(minimize a)
(maximize b)
(check-sat)
(get-model)

wintered · 2022-06-30T23:16:26Z

$z3release model_validate=true tactic.default_tactic=smt sat.euf=true bug.smt2 
sat
(error "line 5 column 10: an invalid model was generated")
$cat bug.smt2                                                                  
(declare-const a Real)
(declare-const b Real)
(assert (not (= 0 b)))
(maximize a)
(check-sat)

NikolajBjorner · 2022-07-01T02:51:45Z

didn't I note before that debugging euf + optimization was a bit early?
Maybe useful to dig into at some point but I am not sure it makes sense to fuzz if I haven't even started testing this.

zhendongsu · 2022-07-01T13:38:50Z

Refutation unsoundness instance:

[616] % z3release small.smt2
sat
[617] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
unsat
[618] % cat small.smt2
(declare-fun a (Int) Int)
(assert (exists ((b Int)) (distinct 0 (a b))))
(assert (forall ((c Int)) (ite (> (a c) 0) true (exists ((d Int)) (= (a c) (+ 1 (a d)))))))
(assert (forall ((c Int)) (or (distinct (a c) 2) (forall ((d Int)) (distinct (a c) (+ 2 (a d)))))))
(assert (forall ((d Int)) (or (= (a d) 5))))
(check-sat)

zhendongsu · 2022-07-01T13:40:34Z

didn't I note before that debugging euf + optimization was a bit early? Maybe useful to dig into at some point but I am not sure it makes sense to fuzz if I haven't even started testing this.

Okay, Nikolaj, no "euf + optimization" for now.

zhendongsu · 2022-07-06T19:46:01Z

[527] % z3release tactic.default_tactic=smt sat.euf=true smt.bv.reflect=false small.smt2
Segmentation fault
[528] % z3debug tactic.default_tactic=smt sat.euf=true smt.bv.reflect=false small.smt2
ASSERTION VIOLATION
File: ../src/ast/euf/euf_enode.h
Line: 164
i < num_args()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[529] % cat small.smt2
(declare-fun a () Int)
(assert (= ((_ int2bv 1) a) (_ bv0 1)))
(check-sat)

merlinsun · 2022-07-18T06:54:11Z

$ z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
failed to verify: (let ((a!1 (store ((as const (Array Bool (Array Bool (Array Int Bool))))
......
$ cat small.smt2
(declare-sort I)
(declare-fun b (Int Int Int Int Int Int) Bool)
(declare-fun o (I I) I)
(declare-fun x () I)
(declare-fun a () (Array Bool (Array Int Bool)))
(assert (forall ((e I)) (exists ((t I)) (and (= e (o e x)) (= t (o x t))))))
(assert (= x (o x x)))
(assert (forall ((v (Array Bool Int)) (va (Array Bool Bool)) (r (Array Bool (Array Bool (Array Int Bool))))) (= r (store r (or (b 1 0 0 1 0 (v (va false)))) a))))
(check-sat)

zhendongsu · 2022-07-18T08:53:15Z

[543] % z3debug small.smt2
unsat
[544] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
false l_true 181: (<= (+ (select #292 0) (* -1.0 #306)) 0.0)
25 l_true l_true 181: (<= (+ (select #292 0) (* -1.0 #306)) 0.0)
0  >= v25
updates 2122
newlits 16 qhead: 16
neweqs  494 qhead: 494
...

ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 622
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[545] % cat small.smt2
(declare-const a Bool)
(declare-const b Bool)
(declare-fun c ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun d ((Array Int (Array Int Real))) (Array Int (Array Int Real)))
(assert (forall ((e Int) (f Int)) (=> (< e f) b)))
(assert (forall ((k Int) (g Int) (h Int) (i Int) (l (Array Int (Array Int Real))) (j (Array Int (Array Int Real)))) (distinct (and (> h g) (> i 0)) (= (select (select (c l (c j (d j))) h) 0) (select (select (c l (c j (d l))) i) k)))))
(assert (or a b))
(check-sat)

wintered · 2022-07-20T14:07:31Z

81cb575

$z3release tactic.default_tactic=smt sat.euf=true bug.smt2                         
[1]    1924299 segmentation fault  z3release tactic.default_tactic=smt sat.euf=true bug.smt2
$cat bug.smt2                                                                      
(assert (forall ((a Real)) (exists ((b Real)) (forall ((c Real)) (exists ((|| Real)) 
        (forall ((d Real)) (exists ((e Real)) (forall ((h Real)) (exists ((f Real)) (let ((g c)) 
        (let ((i d)(j f)) (let ((k j)(l 0))(let ((o (<= a l)))                     
        (let ((m (or o (<= k i)))(n (<= b g))) (or n m)))))))))))))))              
(check-sat)

merlinsun · 2022-07-21T01:48:34Z

Invalid model
81cb575

$ z3 model_validate=true tactic.default_tactic=smt sat.euf=true small.smt2
sat
(error "line 3 column 48: an invalid model was generated")
$ cat small.smt2
(declare-fun e () Real)
(assert (not (xor (= 0.0 0.0) (= e 0) (= e e) (= e 0) (= e e))))
(check-sat-using (then sat-preprocess solve-eqs))

zhendongsu · 2022-07-22T10:01:01Z

Refutation unsoundness:

[532] % z3release model_validate=true small.smt2
sat
[533] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[534] % cat small.smt2
(assert (or true (= (bv2nat ((_ int2bv 3) (bv2nat ((_ int2bv 1) 1)))) (bv2nat ((_ int2bv 1) (bv2nat ((_ int2bv 1) (bv2nat ((_ int2bv 3) 0))))))))) 
(check-sat)

zhendongsu · 2022-07-23T12:59:16Z

Refutation unsoundness:

[617] % z3release model_validate=true small.smt2
sat
[618] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[619] % cat small.smt2
(declare-datatypes ((a 0)) (((b) (c))))
(declare-sort s 0)
(declare-sort t 0)
(declare-fun d (s t) t)
(declare-fun f () t)
(declare-fun m (s t) a)
(declare-fun n (t) Int)
(declare-fun j () Bool)
(assert (forall ((e s)) (distinct b (m e f))))
(assert (forall ((i s) (g s) (h t)) (= (m i (d i h)) (ite (= i g) b c))))
(assert (forall ((h t)) (= (= h f) (distinct 0 (n h)))))
(assert (exists ((i s) (h t)) (distinct (n (d i h)) (ite j 0 (n h)))))
(check-sat)

merlinsun · 2022-07-28T03:30:05Z

This instance relates to #6116 (comment) but is not with smt.bv.reflect=false.

$ z3debug tactic.default_tactic=smt sat.euf=true small2.smt2
ASSERTION VIOLATION
File: ../src/ast/euf/euf_enode.h
Line: 164
i < num_args()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
$ cat small2.smt2
(declare-const x Real)
(assert (forall ((a Real) (v Real) (r Real)) (< (* x (+ v (* x r))) (* (- 1.0 a) (- 1.0 (* v v v))))))
(check-sat-using smt)

merlinsun · 2022-08-05T01:46:44Z

$ cat small2.smt2
(declare-const x Bool)
(declare-fun v () (Array Int Bool))
(declare-fun a () Int)
(assert (or x (= v ((_ map or) v v)) (or (> 1 a) (= 0 (bv2nat ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat ((_ int2bv 3) 7)))))))))))
(check-sat-using smt)
$ z3 small2.smt2 tactic.default_tactic=smt sat.euf=true
Failed to validate 2 25: (= v (map[or] v v)) true
......
ASSERTION VIOLATION
File: ../src/sat/smt/bv_solver.cpp
Line: 656
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

zhendongsu · 2022-08-14T08:45:13Z

FP and the new core:

[515] % z3debug small.smt2
sat
[516] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/ast/fpa/fpa2bv_converter.cpp
Line: 150
f->get_num_parameters() == 1
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[517] % cat small.smt2
(declare-fun a () Float16)
(assert (= a ((_ to_fp 5 11) RTN 65535.0 0)))
(check-sat)

zhendongsu · 2022-08-14T09:01:49Z

Refutation unsoundness:

[618] % z3release model_validate=true small.smt2
sat
[619] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[620] % cat small.smt2
(define-fun a ((b Int)) Int 0)
(declare-fun c (Int) Int)
(declare-fun d (Int) Int)
(assert (or true (= a c) (= a d)))
(assert (= 0 0))
(assert (= (d 0) 1))
(check-sat)

zhendongsu · 2022-08-14T09:47:27Z

[531] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 37 230: (<= (select (select e!3 b!0) 1) 0.0) false
(sat
...
[532] % cat small.smt2
(declare-fun a ((Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun a ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(assert (forall ((b Int) (c Int) (d (Array Int (Array Int Real))) (e (Array Int (Array Int Real)))) (or (= (select (e b) 1) 0) (distinct (select (select (a d d) b) 1) (select (select (a e (a d)) c) 0)))))
(check-sat)

fix unsoundness issue due to book-keeping changes for whether the solver uses assumptions.

handle also nan/oo/0+ as numerals

… logging

…#6116

merlinsun · 2022-08-30T09:23:52Z

Seg fault

$ z3release tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault (core dumped)
$ cat small.smt2
(declare-fun m (Int Int) Bool)
(declare-fun x () Int)
(assert (forall ((e Int)) (distinct (xor (m e 0)) (= 1 (+ x (* e (- 2)))))))
(check-sat)

cd0af99

zhendongsu · 2022-09-01T07:19:37Z

Commit: d3e6ba9

[508] % z3release small.smt2 
unknown
[509] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Segmentation fault
[510] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2 
Segmentation fault
[511] % z3san tactic.default_tactic=smt sat.euf=true small.smt2 
ASAN:DEADLYSIGNAL
=================================================================
==1956==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x55d811ba742b bp 0x7ffe91e77050 sp 0x7ffe91e77010 T0)
==1956==The signal is caused by a READ memory access.
==1956==Hint: address points to the zero page.
    #0 0x55d811ba742a in ast::get_kind() const ../src/ast/ast.h:502
    #1 0x55d811ba742a in is_app_of(expr const*, int, int) ../src/ast/ast.h:1377
    #2 0x55d811ba742a in arith_recognizers::is_numeral(expr const*, rational&, bool&) const ../src/ast/arith_decl_plugin.cpp:699
    #3 0x55d80fefb0e4 in arith_recognizers::is_numeral(expr const*, rational&) const ../src/ast/arith_decl_plugin.h:247
    #4 0x55d80fefb0e4 in mbp::arith_project_plugin::imp::row2expr(u_map<opt::model_based_opt::row> const&, ptr_vector<expr> const&, opt::model_based_opt::row const&) ../src/qe/mbp/mbp_arith.cpp:445
    #5 0x55d80ff053bd in mbp::arith_project_plugin::imp::rows2fmls(vector<opt::model_based_opt::row, true, unsigned int> const&, ptr_vector<expr> const&, ref_vector<expr, ast_manager>&) ../src/qe/mbp/mbp_arith.cpp:517
    #6 0x55d80ff162de in mbp::arith_project_plugin::imp::project(model&, ref_vector<app, ast_manager>&, ref_vector<expr, ast_manager>&, vector<mbp::def, true, unsigned int>&, bool) ../src/qe/mbp/mbp_arith.cpp:390
    #7 0x55d80feeca6e in mbp::arith_project_plugin::operator()(model&, ref_vector<app, ast_manager>&, ref_vector<expr, ast_manager>&) ../src/qe/mbp/mbp_arith.cpp:673
    #8 0x55d80fcfe39e in q::mbqi::solver_project(model&, q::mbqi::q_body&, ref_vector<expr, ast_manager>&, bool) ../src/sat/smt/q_mbi.cpp:318
    #9 0x55d80fd0191e in q::mbqi::check_forall_default(quantifier*, q::mbqi::q_body&, model&) ../src/sat/smt/q_mbi.cpp:190
    #10 0x55d80fd030a5 in q::mbqi::check_forall(quantifier*) ../src/sat/smt/q_mbi.cpp:174
    #11 0x55d80fd0391f in q::mbqi::operator()() ../src/sat/smt/q_mbi.cpp:58
    #12 0x55d80fa6df7f in q::solver::check() ../src/sat/smt/q_solver.cpp:81
    #13 0x55d80fa19600 in operator() ../src/sat/smt/euf_solver.cpp:483
    #14 0x55d80fa19600 in euf::solver::check() ../src/sat/smt/euf_solver.cpp:507
    #15 0x55d81192a3dc in sat::solver::final_check() ../src/sat/sat_solver.cpp:1773
    #16 0x55d81194d340 in sat::solver::basic_search() ../src/sat/sat_solver.cpp:1748
    #17 0x55d81194db61 in sat::solver::bounded_search() ../src/sat/sat_solver.cpp:1735
    #18 0x55d81194eb9f in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1344
    #19 0x55d80fa062d9 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:73
    #20 0x55d80fa0a43b in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:219
    #21 0x55d8109e02bc in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1027
    #22 0x55d8109adf4e in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:153
    #23 0x55d8109af8e7 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:173
    #24 0x55d81081e5d8 in check_sat_core2 ../src/solver/tactic2solver.cpp:229
    #25 0x55d81084205f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #26 0x55d81085b2c4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #27 0x55d81082f7e6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318
    #28 0x55d8107a70a5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1693
    #29 0x55d8107006a3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2611
    #30 0x55d8107006a3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2953
    #31 0x55d8107006a3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3162
    #32 0x55d8106b5985 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3211
    #33 0x55d80d79c331 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:144
    #34 0x55d80d770681 in main ../src/shell/main.cpp:381
    #35 0x7f9211f1ac86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86)
    #36 0x55d80d77d259 in _start (/local/suz-local/software/z3san/build-08312022190913-d3e6ba9/z3+0x1fb259)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:502 in ast::get_kind() const
==1956==ABORTING
[512] % 
[512] % cat small.smt2 
(declare-fun p (Int) Int)
(declare-fun n (Int) Int)
(assert (= 1 (p 0)))
(assert (forall ((s Int) (t Int) (k Int)) (or (= t 0) (> t 0) (= s (- 1)) (distinct k (n (- (div 0 (p k)) t))))))
(check-sat)

NikolajBjorner · 2022-09-03T00:09:21Z

The remaining open issues

NikolajBjorner · 2022-09-03T00:09:50Z

The two last issues are open. Others seem handled. Better to open a new issue for those.

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

fix incorrect mod axiomatization #6116

8ab8b63

NikolajBjorner added a commit that referenced this issue Aug 7, 2022

#6116

8e077d8

NikolajBjorner added a commit that referenced this issue Aug 7, 2022

#6116

410eed9

NikolajBjorner added a commit that referenced this issue Aug 18, 2022

#6116

8e167aa

fix unsoundness issue due to book-keeping changes for whether the solver uses assumptions.

NikolajBjorner added a commit that referenced this issue Aug 18, 2022

#6116

4be26eb

handle also nan/oo/0+ as numerals

NikolajBjorner added a commit that referenced this issue Aug 24, 2022

fix unsoundness in quantifier propagation #6116 and add initial lemma…

ce1f398

… logging

NikolajBjorner added a commit that referenced this issue Aug 24, 2022

fix validator bug returning true for unprocessed case, bug reported in …

c626358

…#6116

NikolajBjorner added a commit that referenced this issue Sep 1, 2022

#6116 bv2int bug fix

6077c41

NikolajBjorner closed this as completed Sep 3, 2022

zhendongsu mentioned this issue Sep 18, 2022

[consolidated] issues in the new core #6319

Closed

wintersteiger mentioned this issue Oct 29, 2023

Assorted fixes for floats #6968

Merged

numinit mentioned this issue Oct 17, 2024

z3: 4.8.17 -> 4.13.4; z3_4_12: 4.12.5 -> 4.12.6 NixOS/nixpkgs#327052

Merged

13 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[consolidated] issues in the new core #6116

[consolidated] issues in the new core #6116

zhendongsu commented Jun 28, 2022

zhendongsu commented Jun 28, 2022

merlinsun commented Jun 29, 2022

merlinsun commented Jun 29, 2022 •

edited

Loading

wintered commented Jun 29, 2022 •

edited

Loading

wintered commented Jun 29, 2022 •

edited

Loading

zhendongsu commented Jun 30, 2022

wintered commented Jun 30, 2022

NikolajBjorner commented Jul 1, 2022

zhendongsu commented Jul 1, 2022

zhendongsu commented Jul 1, 2022

zhendongsu commented Jul 6, 2022

merlinsun commented Jul 18, 2022

zhendongsu commented Jul 18, 2022

wintered commented Jul 20, 2022

merlinsun commented Jul 21, 2022

zhendongsu commented Jul 22, 2022

zhendongsu commented Jul 23, 2022

merlinsun commented Jul 28, 2022 •

edited

Loading

merlinsun commented Aug 5, 2022

zhendongsu commented Aug 14, 2022

zhendongsu commented Aug 14, 2022

zhendongsu commented Aug 14, 2022

merlinsun commented Aug 30, 2022

zhendongsu commented Sep 1, 2022

NikolajBjorner commented Sep 3, 2022

NikolajBjorner commented Sep 3, 2022

[consolidated] issues in the new core #6116

[consolidated] issues in the new core #6116

Comments

zhendongsu commented Jun 28, 2022

zhendongsu commented Jun 28, 2022

merlinsun commented Jun 29, 2022

merlinsun commented Jun 29, 2022 • edited Loading

wintered commented Jun 29, 2022 • edited Loading

wintered commented Jun 29, 2022 • edited Loading

zhendongsu commented Jun 30, 2022

wintered commented Jun 30, 2022

NikolajBjorner commented Jul 1, 2022

zhendongsu commented Jul 1, 2022

zhendongsu commented Jul 1, 2022

zhendongsu commented Jul 6, 2022

merlinsun commented Jul 18, 2022

zhendongsu commented Jul 18, 2022

wintered commented Jul 20, 2022

merlinsun commented Jul 21, 2022

zhendongsu commented Jul 22, 2022

zhendongsu commented Jul 23, 2022

merlinsun commented Jul 28, 2022 • edited Loading

merlinsun commented Aug 5, 2022

zhendongsu commented Aug 14, 2022

zhendongsu commented Aug 14, 2022

zhendongsu commented Aug 14, 2022

merlinsun commented Aug 30, 2022

zhendongsu commented Sep 1, 2022

NikolajBjorner commented Sep 3, 2022

NikolajBjorner commented Sep 3, 2022

merlinsun commented Jun 29, 2022 •

edited

Loading

wintered commented Jun 29, 2022 •

edited

Loading

wintered commented Jun 29, 2022 •

edited

Loading

merlinsun commented Jul 28, 2022 •

edited

Loading