[Consolidated] issues affecting tactic.default_tactic=smt sat.euf=true #5454

rainoftime · 2021-08-04T03:48:52Z

Hi, for the following formula,
z3 9398601

(declare-fun y () Int)
(declare-fun c () (Seq Int))
(declare-fun b () (Seq Int))
(assert (forall ((x Int)) (and (= (seq.nth c y) (seq.nth c 0)) (not (= (seq.nth c x) (seq.nth b x))))))
(check-sat)

ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 594
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

NB: strings are not supported in the new core yet.
This hits some debug code that performs evaluation with respect to strings (sequences) being interpreted and starts complaining. It is not too useful to look for bugs with unsupported interpreted theories because the debug check is not as permissive to consider this.

--
(thanks for the explanation!

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

rainoftime · 2021-08-04T03:49:32Z

stack overflow

(declare-fun RM2 () RoundingMode)
(assert (= RM2 RM2))
(check-sat)

    #1 0x55fe296c115d in str_hash_proc::operator()(char const*) const ../src/util/str_hashtable.h:27
    #2 0x55fe2c126576 in core_hashtable<ptr_hash_entry<char const>, str_hash_proc, str_eq_proc>::get_hash(char const* const&) const ../src/util/hashtab
le.h:152
    #3 0x55fe2c1260ea in core_hashtable<ptr_hash_entry<char const>, str_hash_proc, str_eq_proc>::find_core(char const* const&) const ../src/util/hashta
ble.h:506
    #4 0x55fe2c125526 in core_hashtable<ptr_hash_entry<char const>, str_hash_proc, str_eq_proc>::contains(char const* const&) const ../src/util/hashtab
le.h:531
    #5 0x55fe2c124cbf in is_debug_enabled(char const*) ../src/util/debug.cpp:75
    #6 0x55fe2bb2233b in heap<var_queue::lt>::insert(int) ../src/util/heap.h:235
    #7 0x55fe2bb1aa07 in var_queue::mk_var_eh(unsigned int) ../src/util/var_queue.h:55
    #8 0x55fe2bad62c6 in sat::solver::mk_var(bool, bool) ../src/sat/sat_solver.cpp:317
    #9 0x55fe2aac1a69 in sat::dual_solver::ext2var(unsigned int) ../src/sat/smt/sat_dual_solver.cpp:69
    #10 0x55fe2aac1cad in sat::dual_solver::track_relevancy(unsigned int) ../src/sat/smt/sat_dual_solver.cpp:79
    #11 0x55fe2a9d69aa in euf::solver::track_relevancy(unsigned int) ../src/sat/smt/euf_relevancy.cpp:63
    #12 0x55fe2a9db37e in euf::solver::attach_lit(sat::literal, expr*) ../src/sat/smt/euf_internalize.cpp:168

rainoftime · 2021-08-04T03:53:58Z

Invalid model for FP formula

(set-option :sat.branching.heuristic chb)
(declare-fun A () (Array (_ FloatingPoint 2 3) (_ FloatingPoint 2 2)))
(declare-fun A2 () (Array (_ FloatingPoint 2 3) (_ FloatingPoint 2 2)))
(assert (and (not (= A A2)) (= (select A (_ +oo 2 3)) (select A (_ -oo 2 3)))))
(check-sat)

Failed to validate 13 30: (= (select A +oo) (select A -oo)) false
27: (select A +oo)
(_ -oo 2 2)
29: (select A -oo)
(_ NaN 2 2)
sat

rainoftime · 2021-08-04T04:01:37Z

Memory leak

(declare-fun symmetric ((Array Int (Array Int Real)) Int) Bool)
(assert (forall ((?n Int) (?a (Array Int (Array Int Real)))) (= (symmetric ?a ?n) (forall ((?i Int) (?j Int)) (or (< 1 ?j) (not (= ?i ?n)) (= (select (?a ?i) ?j) (select (?a ?j) ?i)))))))
(check-sat)

==3191075==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 40 byte(s) in 5 object(s) allocated from:
    #0 0x7fc1269a6279 in __interceptor_malloc /build/gcc/src/gcc/libsanitizer/asan/asan_malloc_linux.cpp:145
    #1 0x55b07e350e5d in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:273
    #2 0x55b07e2d7522 in region::allocate(unsigned long) ../src/util/region.cpp:28
    #3 0x55b07cce4a21 in q::ematch::mk_justification(unsigned int, q::clause&, euf::enode* const*) ../src/sat/smt/q_ematch.cpp:97
    #4 0x55b07cce7597 in q::ematch::propagate(bool, euf::enode* const*, unsigned int, q::clause&, bool&) ../src/sat/smt/q_ematch.cpp:276
    #5 0x55b07cce6f2d in q::ematch::on_binding(quantifier*, app*, euf::enode* const*, unsigned int, unsigned int, unsigned int) ../src/sat/smt/q_ematch
.cpp:250
    #6 0x55b07cd51048 in q::mam_impl::on_match(quantifier*, app*, unsigned int, euf::enode* const*, unsigned int) ../src/sat/smt/q_mam.cpp:3823
    #7 0x55b07cd2631b in q::interpreter::execute_core(q::code_tree*, euf::enode*) ../src/sat/smt/q_mam.cpp:2497
    #8 0x55b07cd42d89 in q::interpreter::execute(q::code_tree*) ../src/sat/smt/q_mam.cpp:2014
    #9 0x55b07cd50596 in q::mam_impl::propagate() ../src/sat/smt/q_mam.cpp:3787
    #10 0x55b07ccebbf1 in q::ematch::propagate(bool) ../src/sat/smt/q_ematch.cpp:529
    #11 0x55b07cc55883 in q::solver::unit_propagate() ../src/sat/smt/q_solver.cpp:105
    #12 0x55b07cb44c1d in euf::solver::unit_propagate() ../src/sat/smt/euf_solver.cpp:343
    #13 0x55b07dc72278 in sat::solver::propagate_core(bool) ../src/sat/sat_solver.cpp:1034
    #14 0x55b07dc7257c in sat::solver::propagate(bool) ../src/sat/sat_solver.cpp:1046

rainoftime · 2021-08-04T05:31:51Z

Possibly refutational soudness

(declare-const x Int)
(define-funs-rec ((f () Int) (pred ((y Int)) Bool)) (0 (ite false true (pred x))))
(assert (not (pred 0)))
(check-sat)

the original formula

(define-funs-rec (
(f () Int)
(pred ((y Int)) Bool)) (
0
(ite (< y 0) false (ite (= y 0) true (pred (- y 2))))
))
(assert (not  (pred 5)))
(check-sat)

rainoftime · 2021-08-04T08:58:37Z

src/util/var_queue.h:76

(declare-sort U)
(declare-fun ffk () U)
(declare-fun c (U U) U)
(declare-fun ff () U)
(declare-fun app (U Int) Int)
(assert (and (forall ((f U) (g U)) (not (forall ((x Int)) (not (= (app f x) (app g x)))))) (forall ((x Int)) (= (* x) (app ff x))) (forall ((x Int)) (= (app ffk x) x)) (forall ((f U) (g U) (x Int)) (not (= (app g x) (app (c f g) x))))))
(check-sat)

ASSERTION VIOLATION
File: ../src/util/var_queue.h
Line: 76
!empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

NB: this was a good catch.

rainoftime · 2021-08-04T09:11:44Z

Refutation soundness (without recursive function, but might be redundant with #5454 (comment))

(declare-fun p (Int Int) Bool)
(assert (forall ((x Int) (y Int)) (xor (and (<= 0 y) (<= y x)) (p x y))))
(check-sat)

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

rainoftime · 2021-08-06T06:20:20Z

src/util/vector.h:479

(declare-sort S0)
(declare-fun arr-7575740547724575015_1595139601661751534-0 () (Array Bool (Array Int Int)))
(declare-sort S1)
(declare-fun arr--4150643338936819323_-2156646516907760407-0 () (Array S0 (Array Bool (Array Int Int))))
(declare-fun arr--4150643338936819323_3598003500231606762-0 () (Array S0 (Array S0 (Array Bool (Array Int Int)))))
(declare-fun arr--4150643338935736798_1481373571362265372-0 () (Array S1 (Array S1 S1)))
(declare-fun arr-1481373571362265372_3598003500231606762-0 () (Array (Array S1 S1) (Array S0 (Array Bool (Array Int Int)))))
(declare-fun arr-1481373571362265372_3155022827129298466-0 () (Array (Array S1 S1) (Array (Array S1 S1) (Array S0 (Array Bool (Array Int Int))))))
(declare-fun S1-0 () S1)
(declare-fun arr-3598003500231606762_-7883597554349705702-0 () (Array (Array S0 (Array Bool (Array Int Int))) (Array (Array S1 S1) (Array (Array S1 S1) (Array S0 (Array Bool (Array Int Int)))))))
(declare-fun arr--2156646516907760407_5168333755238154943-0 () (Array (Array Bool (Array Int Int)) (Array (Array S0 (Array S0 (Array Bool (Array Int Int)))) (Array S1 S1))))
(assert (= arr-3598003500231606762_-7883597554349705702-0 (store (store arr-3598003500231606762_-7883597554349705702-0 (select arr-1481373571362265372_3598003500231606762-0 (select arr--4150643338935736798_1481373571362265372-0 S1-0)) arr-1481373571362265372_3155022827129298466-0) arr--4150643338936819323_-2156646516907760407-0 (store arr-1481373571362265372_3155022827129298466-0 (select (select arr--2156646516907760407_5168333755238154943-0 arr-7575740547724575015_1595139601661751534-0) arr--4150643338936819323_3598003500231606762-0) arr-1481373571362265372_3598003500231606762-0))))
(check-sat)

ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 479
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

rainoftime · 2021-08-06T06:29:13Z

src/ast/euf/euf_egraph.cpp:523

(set-logic QF_BV)
(declare-fun bv_28-0 () (_ BitVec 7))
(assert (= bv_28-0 (_ bv0 7)))
(push 4)
(push 3)
(pop 6)
(assert (distinct bv_28-0 (_ bv0 7) ((_ rotate_left 1) bv_28-0)))
(push)
(check-sat)

ASSERTION VIOLATION
File: ../src/ast/euf/euf_egraph.cpp
Line: 523
m_num_scopes == 0 || m_to_merge.empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

zhendongsu · 2021-08-06T20:48:58Z

Regression from z3-4.8.12:

[621] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[622] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 174
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[623] % z3-4.8.12 tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
[624] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert
 (forall ((e Real))
  (or (<= c (* a c))
   (and (< 0.0 (/ 2.0 e))
    (=
     (forall ((e Real))
      (not (forall ((e Real)) (< 0.0 d))))
     (=>
      (and (< 0.0 d)
       (forall ((e Real)) (< 0.0 (/ 2.0 e b))))
      (forall ((e Real)) (= a 0.0))))))))
(assert (forall ((f Real)) (> 0.0 (* a c))))
(check-sat)
[625] %

zhendongsu · 2021-08-06T20:50:52Z

Regression from z3-4.8.10:

[632] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[633] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 846
is_registered_var(v)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[634] % z3-4.8.12 tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[635] % z3-4.8.11 tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[636] % z3-4.8.10 tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
[637] % cat small.smt2
(declare-fun a () Int)
(assert (<= (- a a) 0 (div a 0)))
(check-sat)
[638] %

rainoftime · 2021-08-07T03:39:00Z

heap-use-after-free at vector.h:401

(set-option :rewriter.eq2ineq true)
(set-option :rewriter.arith_ineq_lhs true)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun r0 () Real)
(declare-fun r2 () Real)
(declare-fun r4 () Real)
(declare-fun r5 () Real)
(declare-fun r6 () Real)
(declare-fun v2 () Bool)
(declare-fun r7 () Real)
(declare-fun arr-8446022221574193583_-3731153459322177460-0 () (Array Bool Real))
(declare-fun v3 () Bool)
(declare-fun r8 () Real)
(declare-fun arr--1040333714687977167_7595261608970976177-0 () (Array (Array Bool Bool) (Array (Array (Array (Array (Array Bool Bool) Bool) (Array Bool Bool)) (Array (Array Bool Bool) Bool)) (Array (Array (Array (Array Bool Bool) Bool) (Array Bool Bool)) (Array (Array Bool Bool) Bool)))))
(declare-fun r9 () Real)
(declare-fun arr--3731153459322177460_1895025854887633891-0 () (Array Real (Array (Array (Array (Array Bool Bool) Bool) (Array Bool Bool)) (Array Bool Bool))))
(declare-fun arr--4652642590219547407_-3828347088985530766-0 () (Array (Array (Array Bool Bool) (Array (Array (Array (Array (Array Bool Bool) Bool) (Array Bool Bool)) (Array (Array Bool Bool) Bool)) (Array (Array (Array (Array Bool Bool) Bool) (Array Bool Bool)) (Array (Array Bool Bool) Bool)))) (Array Real (Array (Array (Array (Array Bool Bool) Bool) (Array Bool Bool)) (Array Bool Bool)))))
(declare-fun v20 () Bool)
(assert (or v3 (< 1.0 (select (store arr-8446022221574193583_-3731153459322177460-0 true 0.0) (xor (and (= v2 v1) (= v1 (and (= v0 (and (= (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0) arr-8446022221574193583_-3731153459322177460-0) (= arr-8446022221574193583_-3731153459322177460-0 (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0)))) (= (and (= (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0) arr-8446022221574193583_-3731153459322177460-0) (= arr-8446022221574193583_-3731153459322177460-0 (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0))) v3) (= v3 v0) (= v0 v2))) (= (and (= v0 (and (= (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0) arr-8446022221574193583_-3731153459322177460-0) (= arr-8446022221574193583_-3731153459322177460-0 (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0)))) (= (and (= (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0) arr-8446022221574193583_-3731153459322177460-0) (= arr-8446022221574193583_-3731153459322177460-0 (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0))) v3) (= v3 v0) (= v0 v2)) (and (= (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0) arr-8446022221574193583_-3731153459322177460-0) (= arr-8446022221574193583_-3731153459322177460-0 (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0)))) (= (and (= (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0) arr-8446022221574193583_-3731153459322177460-0) (= arr-8446022221574193583_-3731153459322177460-0 (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0))) v3)) (= (select arr-8446022221574193583_-3731153459322177460-0 v1) r0) (and (= v2 v1) (= v1 (and (= v0 (and (= (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0) arr-8446022221574193583_-3731153459322177460-0) (= arr-8446022221574193583_-3731153459322177460-0 (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0)))) (= (and (= (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0) arr-8446022221574193583_-3731153459322177460-0) (= arr-8446022221574193583_-3731153459322177460-0 (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0))) v3) (= v3 v0) (= v0 v2))) (= (and (= v0 (and (= (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0) arr-8446022221574193583_-3731153459322177460-0) (= arr-8446022221574193583_-3731153459322177460-0 (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0)))) (= (and (= (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0) arr-8446022221574193583_-3731153459322177460-0) (= arr-8446022221574193583_-3731153459322177460-0 (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0))) v3) (= v3 v0) (= v0 v2)) (and (= (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0) arr-8446022221574193583_-3731153459322177460-0) (= arr-8446022221574193583_-3731153459322177460-0 (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0)))) (= (and (= (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0) arr-8446022221574193583_-3731153459322177460-0) (= arr-8446022221574193583_-3731153459322177460-0 (store (store arr-8446022221574193583_-3731153459322177460-0 v1 r6) v0 r0))) v3)))))))
(assert (= (select arr-8446022221574193583_-3731153459322177460-0 v1) r0))
(assert (or (= r7 1.0) (and (= 1.0 r8) (< r8 0.0) (= r8 r5) (< (abs r7) (+ r8 (- 0.0 r9 r9 r4))))))
(assert (or v20 (and (= r8 r2) (< 1.0 r6)) (and (= (store arr--4652642590219547407_-3828347088985530766-0 arr--1040333714687977167_7595261608970976177-0 arr--3731153459322177460_1895025854887633891-0) arr--4652642590219547407_-3828347088985530766-0) (= arr--4652642590219547407_-3828347088985530766-0 (store arr--4652642590219547407_-3828347088985530766-0 arr--1040333714687977167_7595261608970976177-0 arr--3731153459322177460_1895025854887633891-0)))))
(apply (and-then simplify reduce-invertible sat-preprocess))

rainoftime · 2021-08-07T07:58:44Z

src/sat/smt/euf_invariant.cpp:59

(set-option :rewriter.expand_nested_stores true)
(declare-sort Element)
(declare-sort Index)
(declare-fun e6 () Element)
(declare-fun i6 () Index)
(declare-fun i2 () Index)
(declare-fun i4 () Index)
(declare-fun e9 () Element)
(declare-fun i8 () Index)
(declare-fun i10 () Index)
(declare-fun a1 () (Array Index Element))
(assert (exists ((i3 Index)) (and (= i3 i8) (= i6 i10) (not (= (store (store (store a1 i4 e9) i2 e6) i10 e6) (store (store (store a1 i6 e9) i8 e6) i10 e9))))))
(check-sat-using lira)

$ z3 dd.smt2 
sat
$ z3 tactic.default_tactic=smt sat.euf=true dd.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/euf_invariant.cpp
Line: 59
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

rainoftime · 2021-08-08T09:44:32Z

src/math/lp/lar_core_solver.h:732

(declare-fun r3 () Real)
(declare-fun arr0 () (Array Real Bool))
(declare-fun arr1 () (Array (Array Real Bool) Real))
(assert (= arr0 (store arr0 r3 true)))
(assert (< 57932588.0 (* (select arr1 arr0) (select arr1 arr0))))
(assert (= (store arr0 57932588.0 true) (store arr0 1.0 false)))
(check-sat)

ASSERTION VIOLATION
File: ../src/math/lp/lar_core_solver.h
Line: 732
l <= u
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

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

@wintersteiger

@wintersteiger: added code review comment to theory_fpa. The bug seen in #5454 doesn't surface with theory_fpa, though.

NikolajBjorner · 2021-08-15T23:50:17Z

Another formula

(declare-fun a_146 () (Array Int Int))
(declare-fun a_98 () (Array Int Int))
(declare-fun a_144 () (Array Int Int))
(assert (and (= a_98 (store a_98 1 0)) (= a_146 (store a_98 0 0)) (not (= a_146 (store a_144 0 0)))))
(check-sat)

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

NikolajBjorner · 2021-08-16T02:14:26Z

these are now all considered. The last couple of fixes were somewhat intrusive and likely to produce at least performance regressions.

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

NikolajBjorner added a commit that referenced this issue Aug 4, 2021

#5454

ed3f8a5

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

NikolajBjorner added a commit that referenced this issue Aug 10, 2021

#5454

7ab7b86

NikolajBjorner added a commit that referenced this issue Aug 11, 2021

#5454

d1d64bb

NikolajBjorner added a commit that referenced this issue Aug 11, 2021

#5454

496ec5f

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

NikolajBjorner added a commit that referenced this issue Aug 11, 2021

#5454

178262f

NikolajBjorner added a commit that referenced this issue Aug 11, 2021

#5454

8faad26

NikolajBjorner added a commit that referenced this issue Aug 11, 2021

#5454

fde8808

NikolajBjorner added a commit that referenced this issue Aug 12, 2021

#5454

4610702

NikolajBjorner added a commit that referenced this issue Aug 12, 2021

#5454

fea1424

NikolajBjorner added a commit that referenced this issue Aug 12, 2021

#5454

b016465

NikolajBjorner added a commit that referenced this issue Aug 15, 2021

#5454

6a3ba64

@wintersteiger: added code review comment to theory_fpa. The bug seen in #5454 doesn't surface with theory_fpa, though.

NikolajBjorner added a commit that referenced this issue Aug 16, 2021

#5454

3d13c03

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

NikolajBjorner added a commit that referenced this issue Aug 16, 2021

#5454

429e5ed

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

rainoftime closed this as completed Aug 16, 2021

NikolajBjorner added a commit that referenced this issue Aug 16, 2021

modify #5454

904c6e2

NikolajBjorner reopened this Aug 18, 2021

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

#5454 again

adcdd11

NikolajBjorner added a commit that referenced this issue Aug 19, 2021

#5454 again

d0e2108

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

NikolajBjorner closed this as completed Aug 24, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Consolidated] issues affecting tactic.default_tactic=smt sat.euf=true #5454

[Consolidated] issues affecting tactic.default_tactic=smt sat.euf=true #5454

rainoftime commented Aug 4, 2021 •

edited

Loading

rainoftime commented Aug 4, 2021 •

edited

Loading

rainoftime commented Aug 4, 2021 •

edited by NikolajBjorner

Loading

rainoftime commented Aug 4, 2021

rainoftime commented Aug 4, 2021

rainoftime commented Aug 4, 2021 •

edited by NikolajBjorner

Loading

rainoftime commented Aug 4, 2021 •

edited

Loading

rainoftime commented Aug 6, 2021

rainoftime commented Aug 6, 2021

zhendongsu commented Aug 6, 2021

zhendongsu commented Aug 6, 2021

rainoftime commented Aug 7, 2021

rainoftime commented Aug 7, 2021

rainoftime commented Aug 8, 2021

NikolajBjorner commented Aug 15, 2021

NikolajBjorner commented Aug 16, 2021

[Consolidated] issues affecting tactic.default_tactic=smt sat.euf=true #5454

[Consolidated] issues affecting tactic.default_tactic=smt sat.euf=true #5454

Comments

rainoftime commented Aug 4, 2021 • edited Loading

rainoftime commented Aug 4, 2021 • edited Loading

rainoftime commented Aug 4, 2021 • edited by NikolajBjorner Loading

rainoftime commented Aug 4, 2021

rainoftime commented Aug 4, 2021

rainoftime commented Aug 4, 2021 • edited by NikolajBjorner Loading

rainoftime commented Aug 4, 2021 • edited Loading

rainoftime commented Aug 6, 2021

rainoftime commented Aug 6, 2021

zhendongsu commented Aug 6, 2021

zhendongsu commented Aug 6, 2021

rainoftime commented Aug 7, 2021

rainoftime commented Aug 7, 2021

rainoftime commented Aug 8, 2021

NikolajBjorner commented Aug 15, 2021

NikolajBjorner commented Aug 16, 2021

rainoftime commented Aug 4, 2021 •

edited

Loading

rainoftime commented Aug 4, 2021 •

edited

Loading

rainoftime commented Aug 4, 2021 •

edited by NikolajBjorner

Loading

rainoftime commented Aug 4, 2021 •

edited by NikolajBjorner

Loading

rainoftime commented Aug 4, 2021 •

edited

Loading