I am processing the output of Z3 with regexs for various scripts I use to conduct experiments. I ran into a bug in my scripts today when certain inputs cause Z3 to finish "in zero time".
Id #105 | Release:
| Updated: Apr 8 at 1:18 PM by switicus | Created: Apr 8 at 11:30 AM by switicus
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 4:32 PM by LeventErkok | Created: Feb 15 at 4: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: Mar 24 at 10:46 PM by Heizmann | Created: Feb 13 at 5: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: Mar 20 at 4:02 AM by NBjorner | Created: Nov 26, 2013 at 8: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 2:25 PM by ic3guy | Created: Oct 15, 2013 at 10:21 AM by ic3guy
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 6:47 PM by NikolajBjorner | Created: May 29, 2013 at 5: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 7:19 PM by dvitek | Created: Feb 6, 2013 at 5: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 10:52 PM by rybal | Created: Oct 9, 2012 at 9:44 AM by Adorf