Swire42
Swire42
# The problem Unlike `--info=progress`, `--info=progress2` does not insert newlines after each transferred file. This is a problem because `progress2` displays 2 different kinds of information: - During file transfer...
The implementation of Blarney.Vector.drop was incorrect, it always produced an empty list.
I'm trying to cross-compile my crate, which depends on `freetype-sys`, from Linux to macOS. When I run `cargo build --target x86_64-apple-darwin`, the compilation of freetype-sys fails very much like https://github.com/gfx-rs/wgpu/issues/2956....
This pull request builds on #135 (#133 + #134), and adds two more key features: - A new verification scheme, that makes use of quantifiers to significantly reduce the required...
After running into a [z3 performance issue](https://github.com/Z3Prover/z3/issues/7207) triggered by the complex SMT scripts that the current Blarney SMT backend generates, I decided to write a new SMT backend. # Example...
It has come to my attention that in various places, Blarney uses the assumption that "DontCare can be treated as 0". While that might be very fine when one just...
This builds on #133 and #134 to provide proper verification of don't care values. Look at these pull requests first. This new verification was tested to work on the following...
The following input: ``` (push) (declare-datatype Pair ((mkPair (fst Bool) (snd Bool)))) (assert (= (fst (mkPair true false)) (fst (mkPair false false)))) (check-sat) (pop) (push) (declare-datatype Pair ((mkPair (snd Bool)...
I ran into a huge performance issue using datatypes, bitvectors, and shallow linear recursion (depth
### Error message The following program fails to compile and crashes the game: ``` public class A { void A() {} } public class B { static A a =...