ASSERTION VIOLATION: c == not_l @ sat_solver.cpp:611
This issue has the same symptom an issue 61, but a different input.
End of master branch built with Z3DEBUG=1 and _EXTERNAL_RE...
Id #93 | Release:
| Updated: Feb 26 at 1:02 PM by wintersteiger | Created: Feb 21 at 8:17 PM by dvitek
I'm trying to follow the unstable-branch on OS-X closely. It appears that the last 15 nightly builds are all called the same:
I thought the h...
Id #91 | Release:
| Updated: Feb 15 at 5:32 PM by LeventErkok | Created: Feb 15 at 5:32 PM by LeventErkok
The following two line SMT-LIB seems to be correct according to the AUFNIRA definition.
since (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_r...
Id #90 | Release:
| Updated: Feb 13 at 6:54 PM by Heizmann | Created: Feb 13 at 6:54 PM by Heizmann
We sometimes use a logic comprised of QF_ABV plus the "as const" array construct. I recently did an experiment where I extended z3 with a QF_GABV logic (GA = Generalized Arrays). I added...
Id #78 | Release:
| Updated: Nov 26, 2013 at 9:10 PM by dvitek | Created: Nov 26, 2013 at 9:10 PM by dvitek
In our work with MetiTarski and z3, we use the :timeout option for calls of (check-sat-using). Many repeated calls to z3 (4.3.1) are taking place. With OSX 10.8.5 and XCode 5, if you repeatedly cal...
Id #70 | Release:
| Updated: Oct 15, 2013 at 3:25 PM by ic3guy | Created: Oct 15, 2013 at 11:21 AM by ic3guy
I am working with Z3 and have noticed a strage behaviour while I was working with arrays. Because nobody on Stackoverflow could or wanted to answer my question and the behaviour seems so st...
Id #59 | Release:
| Updated: Aug 1, 2013 at 9:28 AM by cliguda | Created: Aug 1, 2013 at 9:28 AM by cliguda
I posted a stackoverflow question on this topic; as yet it's unanswered, but my subsequent experience makes me think more and more that this is a bug. Here is the original question:
Id #55 | Release:
| Updated: Jul 16, 2013 at 9:12 PM by NikolajBjorner | Created: Jul 15, 2013 at 1:09 PM by EfForEffort
I think we're basically seeing the windows version of issue 21 here. If the timeout timer goes off while the main thread is holding a heap lock (perhaps because it is executing malloc or free), th...
Id #42 | Release:
| Updated: Jun 2, 2013 at 7:47 PM by NikolajBjorner | Created: May 29, 2013 at 6:53 PM by dvitek
On platforms where z3 uses signals to implement timeouts (anything but mac/windows), z3 has a race where it can run into problems when it invokes non-async-signal-safe functions from inside the tim...
Id #21 | Release:
| Updated: Feb 7, 2013 at 8:19 PM by dvitek | Created: Feb 6, 2013 at 6:35 PM by dvitek
When I submit the attached file with a SMT-problem description for the n-queens problem with n=4 to Z3 4.1.2 (downloaded yesterday, the z3 /version reports V4.2, though), I get an unknown upon the ...
Id #2 | Release:
| Updated: Jan 24 at 11:52 PM by rybal | Created: Oct 9, 2012 at 10:44 AM by Adorf