This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(set-info :source | fuzzsmt 0.3 |) | |
(set-logic QF_ABV) | |
(set-info :status unknown) | |
(declare-fun v0 () (_ BitVec 10)) | |
(declare-fun v1 () (_ BitVec 4)) | |
(declare-fun v2 () (_ BitVec 12)) | |
(declare-fun v3 () (_ BitVec 8)) | |
(declare-fun v4 () (_ BitVec 12)) | |
(declare-fun a5 () (Array (_ BitVec 11) (_ BitVec 3))) | |
(declare-fun a6 () (Array (_ BitVec 2) (_ BitVec 3))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
valgrind -q --leak-check=full --error-exitcode=9 ../../build/cryptominisat4 --zero-exit-status --reconf 9 --reconfat 1 --burst 0 --restart luby --gluehist 36 --updateglueonprop 1 --updateglueonanalysis 0 --otfhyper 0 --clearstat 1 --cacheformoreminim 1 --stampformoreminim 1 --maxredratio 17 --dompickf 18 --alwaysmoremin 1 --rewardotfsubsume 51 --bothprop 1 --probemaxm 1000 --cachesize 68 --calcreach 1 --cachecutoff 1269 --elimstrgy calculate --elimcplxupd 0 --occredmax 76 --noextbinsubs 0 --extscc 1 --distill 0 --sortwatched 1 --recur 1 --compsfrom 0 --compsvar 298891 --compslimit 2925 --implicitmanip 0 --occsimp 0 --occirredmaxmb 8 --occredmaxmb 6 --skipresol 1 --implsubsto 0 --sync 6000 -m 0.508328742011 --verb 0 --threads 1 --preproc 1 fuzzTest_1.cnf fuzzTest_1.cnf-simplified.cnf --savedstate fuzzTest_1.cnf-simplified.cnf-savedstate.dat | |
Error line while executing: ==11981== 32 bytes in 1 blocks are definitely lost in loss record 118 of 737 | |
Error line while executing: ==11981== at 0x4C29180: oper |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/bin/bash | |
set -e | |
set -x | |
sudo yum -y groupinstall 'Development Tools' | |
sudo yum -y install boost-devel | |
sudo yum -y install cmake | |
sudo yum -y install zlib-devel | |
sudo yum -y install boost-static | |
sudo yum -y install libstdc++-static |
This file has been truncated, but you can view the full file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
p cnf 9152 188536 | |
c Key vars: [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128] | |
c Plaintex vars: [129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 21 |