John Regehr on Nostr: this is silly, I used to be a pretty heavy user of the Python Z3 bindings but it's ...
this is silly, I used to be a pretty heavy user of the Python Z3 bindings but it's been a few years. after updating code that I'm pretty sure used to work for Python3, my exists-forall queries aren't working, I'm getting a nonsensical 0 printed by this program instead of the correct answer: 2. anyone happen to know what I'm doing wrong?
https://gist.github.com/regehr/aab68b20863e1a86327911eda8ec79aePublished at
2024-11-21 18:25:38Event JSON
{
"id": "acc7dfb31dce5da0b01f2d3f3d2a4681297d8cd3ae333931253cfa13946e3777",
"pubkey": "a1a4eb540235341a2db0d8a08cfb74edc4bb06b316c7bb39580c55559ce71ba1",
"created_at": 1732213538,
"kind": 1,
"tags": [
[
"proxy",
"https://mastodon.social/users/regehr/statuses/113522346467789329",
"activitypub"
]
],
"content": "this is silly, I used to be a pretty heavy user of the Python Z3 bindings but it's been a few years. after updating code that I'm pretty sure used to work for Python3, my exists-forall queries aren't working, I'm getting a nonsensical 0 printed by this program instead of the correct answer: 2. anyone happen to know what I'm doing wrong?\n\nhttps://gist.github.com/regehr/aab68b20863e1a86327911eda8ec79ae",
"sig": "ef68a092df0fc5f22c8c69fd32e36c65b873fee2aa84d520923982a1830090b36d8e0fc6d5e18a6aafe4fb29571e1fb6f80c6fd9847dedf15812004dba6a84ed"
}
