 |
Post At9X9jyrf8VB1dAx3Q by [email protected] |
 |
More posts by [email protected] |
|
Post #At9VNhPXoUjhCYBPs0 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
hot take: SMT-LIB is designed by incompetent people for the sole purpose of hav… |
|
|
|
Post #At9VP42RAfl3fV1f9c by [email protected] |
|
0 likes, 0 repeats |
|
|
|
separately from that, Z3 is bad software |
|
|
|
Post #At9VW7e89gZCsx1R4q by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@whitequark opinions on cvc5? Others? |
|
|
|
Post #At9VfzHc6WC9qLC5wm by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@arnaugamez not enough experience to sayZ3 commits several crimes, with one of … |
|
|
|
Post #At9VquxWWMyrcN0clM by [email protected] |
|
0 likes, 0 repeats |
|
|
|
imagine this code stomping on your face foreverthis is the experience of using … |
|
|
|
Post #At9W7VxQjHJt03sZyi by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@whitequark It's Python, isn't it? |
|
|
|
Post #At9W81YjEeZh0iZIv2 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
if SMT-LIB was designed for actually useful applications it would have had a fu… |
|
|
|
Post #At9WBfqxsZRmqiq3ii by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@soc no? SMT-LIB is its own language, vaguely lispy in nature |
|
|
|
Post #At9WG7XKtXjxrlmHRY by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@whitequark Ah, thank you!I was confused by later comments in the thread. |
|
|
|
Post #At9WH0rnBBmdT8ltSq by [email protected] |
|
0 likes, 0 repeats |
|
|
|
every time i have to interact with SMT solvers it leaves me incandescently angr… |
|
|
|
Post #At9WSgdIEaNEBpYXNg by [email protected] |
|
0 likes, 0 repeats |
|
|
|
whose fucking idea was it to require the shift amount to have the same width as… |
|
|
|
Post #At9X9jyrf8VB1dAx3Q by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@whitequark if it is a shift where both the value and the shift amount are in r… |
|
|
|
Post #At9XMTajuMblxZxq88 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@skandhurkat this is completely irrelevant |
|
|
|
Post #At9XcTIGmdGNfYx648 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@whitequark sorry, I misunderstood the context |
|
|
|
Post #At9am0oLprCS5gCOfI by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@whitequark @arnaugamez why operator overloading is a terrible idea pt.174 |
|
|
|
Post #At9am0v5QoaUQZLmAC by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@rasteri @arnaugamez you can do it in a reasonable manner; Amaranth for example… |
|
|
|
Post #At9d9kwChgC1icK0dE by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@[email protected] maybe now you better understand why I think using p… |
|
|
|
Post #At9d9l2aJxIU2PJ6Zs by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ignaloidas i'm all for less crackhead APIs yes |
|
|
|
Post #At9dCDfUr4jrP6gKKe by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ignaloidas SMT doesn't even add that much value. arguably it adds negative… |
|
|
|
Post #AtA73l48JQcr0E5Qm0 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@whitequark :( |
|
|
|
Post #AtA73lAVvhjJK14Wie by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@sandmouth I really wanted to like it! I spent several months trying to make th… |
|
|
|
Post #AtAYx2UnuGEjkc981A by [email protected] |
|
0 likes, 0 repeats |
|
|
|
your query is slow. you have decided to use theory of arraysnow your query does… |
|
|
|
Post #AtAZ81exM7zoLJ8LtA by [email protected] |
|
0 likes, 0 repeats |
|
|
|
instead of: QF_BVAhave you considered: QF_BV and you concatenate all of your sy… |
|
|
|
Post #AtC2PqHHVI2s5Frqro by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@whitequark @ignaloidas SMT is a big tent for both software / hardware verifica… |
|
|
|
Post #AtC2PqPR0yZEUXgMZk by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@[email protected] @[email protected] it's not that SMTLIB doesn&… |
|
|
|
Post #AtC2PqWWacEqqX01cu by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ignaloidas @sandmouth yeah |
