Open
Description
Input
(set-logic HORN)
(declare-fun
main@_6
( Int Int Int ) Bool
)
(declare-fun
main@.preheader
( Int Int Int Int ) Bool
)
(declare-fun
main@.lr.ph
( Int Int ) Bool
)
(assert
(forall
( (A Int) (C Int) (I Int) (J Int) )
(=>
(and
(>= (+ C (* (- 1) J)) 0) (>= (+ I (* (- 1) A)) 1)
(main@.preheader C A I J)
)
(main@.preheader (+ C (- 1)) (+ A 1) I J)
)
)
)
(assert
(forall
( (H Int) (I Int) )
(=>
(and
true
true
)
(main@_6 0 H I)
)
)
)
(assert
(forall
( (A Int) (B Int) (D Int) )
(=>
(and
(not (= D 0))
(main@.lr.ph A B)
)
(main@.lr.ph (+ A 1) (+ B 1))
)
)
)
(assert
(forall
( (B Int) (C Int) (L Int) (M Int) )
(=>
(and
(not (= B 0))
(main@_6 C L M)
)
(main@_6 (+ C 1) L M)
)
)
)
(assert
(forall
( (B Int) (C Int) (D Int) )
(=>
(and
(or (>= (+ C (* (- 1) B)) 1) (>= (+ D (* (- 1) C)) 0))
(main@_6 C B D)
)
(main@.preheader 0 0 (- 1) 1)
)
)
)
(assert
(forall
( (A Int) (B Int) (C Int) (H Int) )
(=>
(and
(or (>= (+ B (* (- 1) A)) 1) (>= (+ C (* (- 1) B)) 0)) (not (= H 0))
(main@_6 B A C)
)
(main@.lr.ph 0 0)
)
)
)
(assert
(forall
( (A Int) (C Int) (D Int) (G Int) )
(=>
(and
(>= (+ G (* (- 1) A)) 2) (>= (+ D (* (- 1) C)) 1)
(main@.preheader (+ A 1) C D G)
)
false
)
)
)
(assert
(forall
( (B Int) (I Int) )
(=>
(and
true
(main@.lr.ph I B)
)
(main@.preheader (+ B 1) 0 I 1)
)
)
)
(check-sat)
Output (sometimes)
hoice(62406,0x70000f03c000) malloc: *** error for object 0x600002c34bb0: pointer being freed was not allocated
hoice(62406,0x70000f03c000) malloc: *** set a breakpoint in malloc_error_break to debug
fish: Job 1, './target/release/hoice --log_...' terminated by signal SIGABRT (Abort)Version
macOS Monterey 12.2.1
hoice 1.8.1 (manually built(1c9a5d110 2021-01-29)
z3 4.8.13
rustc 1.60.0
This error doesn't happen on Debian 11, z3 4.8.13, rustc 1.57.0
Stack Trace
hoice(63567,0x70000b73a000) malloc: *** error for object 0x600003500000: pointer being freed was not allocated
hoice(63567,0x70000b73a000) malloc: *** set a breakpoint in malloc_error_break to debug
thread #2, name = 'ice', stop reason = signal SIGABRT
frame #0: 0x00007ff805dd0112 libsystem_kernel.dylib`__pthread_kill + 10
frame #1: 0x00007ff805e06214 libsystem_pthread.dylib`pthread_kill + 263
frame #2: 0x00007ff805d52d10 libsystem_c.dylib`abort + 123
frame #3: 0x00007ff805c303e2 libsystem_malloc.dylib`malloc_vreport + 548
frame #4: 0x00007ff805c335ed libsystem_malloc.dylib`malloc_report + 151
frame #5: 0x00000001002754b7 hoice`hoice::data::Data::destroy::hb59ed86746733263 + 2887
frame #6: 0x00000001000c77a3 hoice`hoice::learning::ice::IceLearner::learn::h4fa19c30151517de + 1283
frame #7: 0x00000001000c6238 hoice`hoice::learning::ice::IceLearner::run::h847aee6c547ef342 + 1800
frame #8: 0x00000001000c43a4 hoice`hoice::learning::ice::Launcher::launch::h86dedf9dfc6a0166 + 436
frame #9: 0x0000000100336752 hoice`std::sys_common::backtrace::__rust_begin_short_backtrace::hf1caa9859d2433f7 + 162
frame #10: 0x000000010019faa2 hoice`core::ops::function::FnOnce::call_once$u7b$$u7b$vtable.shim$u7d$$u7d$::h3fd6720881912218 + 178
frame #11: 0x00000001003de767 hoice`std::sys::unix::thread::Thread::new::thread_start::h9b70539161da4eaf [inlined] _$LT$alloc..boxed..Box$LT$F$C$A$GT$$u20$as$u20$core..ops..function..FnOnce$LT$Args$GT$$GT$::call_once::h76ed59d8775c95eb at boxed.rs:1853:9 [opt]
frame #12: 0x00000001003de761 hoice`std::sys::unix::thread::Thread::new::thread_start::h9b70539161da4eaf [inlined] _$LT$alloc..boxed..Box$LT$F$C$A$GT$$u20$as$u20$core..ops..function..FnOnce$LT$Args$GT$$GT$::call_once::h9a39ecfa1322b383 at boxed.rs:1853:9 [opt]
frame #13: 0x00000001003de75a hoice`std::sys::unix::thread::Thread::new::thread_start::h9b70539161da4eaf at thread.rs:108:17 [opt]
frame #14: 0x00007ff805e064f4 libsystem_pthread.dylib`_pthread_start + 125
frame #15: 0x00007ff805e0200f libsystem_pthread.dylib`thread_start + 15
libsystem_kernel.dylib`__pthread_kill:
0x7ff805dd0108 <+0>: movl $0x2000148, %eax ; imm = 0x2000148
0x7ff805dd010d <+5>: movq %rcx, %r10
0x7ff805dd0110 <+8>: syscall
-> 0x7ff805dd0112 <+10>: jae 0x7ff805dd011c ; <+20>
0x7ff805dd0114 <+12>: movq %rax, %rdi
0x7ff805dd0117 <+15>: jmp 0x7ff805dca2f1 ; cerror_nocancel
0x7ff805dd011c <+20>: retq
0x7ff805dd011d <+21>: nop
0x7ff805dd011e <+22>: nop
0x7ff805dd011f <+23>: nop
rax = 0x0000000000000000
rdx = 0x0000000000000000
rbx = 0x000070000b73a000
rbp = 0x000070000b737ab0
rsp = 0x000070000b737a88Metadata
Metadata
Assignees
Labels
No labels