Failure of tests on fresh checkout (Mac OS X)

[wbl]

I've just started to get this running, and run into a roadblock:

$pip3.7 show z3-solver Name: z3-solver Version: 4.8.7.0 Summary: an efficient SMT solver library Home-page: https://github.com/Z3Prover/z3 Author: The Z3 Theorem Prover Project Author-email: None License: MIT License Location: /usr/local/lib/python3.7/site-packages Requires: Required-by:
`$python3 runAutoGroup.py --sdl schemes/cl04.sdl --config schemes/configCL.py -o TestCL -v
runAutoGroup.py:3: DeprecationWarning: the imp module is deprecated in favour of importlib; see the module's documentation for alternative uses
import imp
runAutoGroup.py:792: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead
startTime = time.clock()
sdl: 1 name := LRSW
sdl: 2 setting := symmetric
sdl: 3
sdl: 4 BEGIN :: types
sdl: 5 x := ZR
sdl: 6 y := ZR
sdl: 7 z := ZR
sdl: 8 END :: types
sdl: 9
sdl: 10
sdl: 11 BEGIN :: func:setup
sdl: 12 input := None
sdl: 13 x := random(ZR)
sdl: 14 y := random(ZR)
sdl: 15
sdl: 16 g := random(G1)
sdl: 17
sdl: 18 assumpKey := list{g, x, y}
sdl: 19
sdl: 20 output := assumpKey
sdl: 21 END :: func:setup
sdl: 22
sdl: 23
sdl: 24 BEGIN :: func:assump
sdl: 25 input := assumpKey
sdl: 26 assumpKey := expand{g, x, y}
sdl: 27 X := (g^x)
sdl: 28 Y := (g^y)
sdl: 29
sdl: 30 assumpVar := list{X, Y}
sdl: 31
sdl: 32 output := assumpVar
sdl: 33 END :: func:assump
reducing size of 'signature'
<=== Assumption Instance Graph ===>
digraph assumption {
g -> Y
g -> X
g
}

<=== Assumption Instance Graph ===>
16 : G1 :=> g := random(G1) , loop :=> False

runAutoGroup.py:794: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead
endTime = time.clock()
['reductionCL']
runAutoGroup.py:820: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead
startTime = time.clock()
sdl: 1 name := cl04
sdl: 2 setting := symmetric
sdl: 3
sdl: 4 BEGIN :: types
sdl: 5 m := ZR
sdl: 6 END :: types
sdl: 7
sdl: 8 BEGIN :: func:setup
sdl: 9 input := list{assumpKey, assumpVar}
sdl: 10
sdl: 11
sdl: 12 x := random(ZR)
sdl: 13 y := random(ZR)
sdl: 14 g := random(G1)
sdl: 15
sdl: 16 X := (g^x)
sdl: 17 Y := (g^y)
sdl: 18
sdl: 19 reductionKey := list{x, y}
sdl: 20 reductionParams := list{p, g, X, Y}
sdl: 21 output := list{reductionKey, reductionParams}
sdl: 22 END :: func:setup
sdl: 23
sdl: 24
sdl: 25 BEGIN :: func:queries
sdl: 26 input := list{m, reductionParams, reductionKey}
sdl: 27 reductionKey := expand{x, y}
sdl: 28 reductionParams := expand{p, g, X, Y}
sdl: 29
sdl: 30 r := random(ZR)
sdl: 31 a := (g^r)
sdl: 32 b := (a^y)
sdl: 33 c := (a^(x + ((m * x) * y)))
sdl: 34
sdl: 35 sig := list{a, b, c}
sdl: 36
sdl: 37 output := sig
sdl: 38 END :: func:queries
sdl: 39
sdl: 40
reducing size of 'signature'
<=== Reduction Setup Graph ===>
digraph setup {
g
g -> X
g -> Y
}

<=== Reduction Setup Graph ===>
<=== Reduction Query Graph (backward) ===>
digraph queries {
g -> a
a -> b
a -> c
}

<=== Reduction Query Graph (backward) ===>
<=== Reduction Graph ===>
digraph reduction {
g -> Y
a -> c
a -> b
g
g -> a
g -> X
}

<=== Reduction Graph ===>
14 : G1 :=> g := random(G1) , loop :=> False
runAutoGroup.py:822: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead
endTime = time.clock()
runAutoGroup.py:870: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead
startTime = time.clock()
sdl: 1 name := cl04
sdl: 2 setting := symmetric
sdl: 3
sdl: 4 BEGIN :: types
sdl: 5 M := Str
sdl: 6 END :: types
sdl: 7
sdl: 8 BEGIN :: func:setup
sdl: 9 input := list{None}
sdl: 10 g := random(G1)
sdl: 11 output := g
sdl: 12 END :: func:setup
sdl: 13
sdl: 14
sdl: 15 BEGIN :: func:keygen
sdl: 16 input := list{g}
sdl: 17 x := random(ZR)
sdl: 18 y := random(ZR)
sdl: 19 X := (g^x)
sdl: 20 Y := (g^y)
sdl: 21 sk := list{x, y}
sdl: 22 pk := list{X, Y}
sdl: 23 output := list{pk, sk}
sdl: 24 END :: func:keygen
sdl: 25
sdl: 26
sdl: 27 BEGIN :: func:sign
sdl: 28 input := list{g, sk, M}
sdl: 29 sk := expand{x, y}
sdl: 30 r := random(ZR)
sdl: 31 m := H(M,ZR)
sdl: 32 a := (g^r)
sdl: 33 b := (a^y)
sdl: 34 c := (a^(x + ((m * x) * y)))
sdl: 35 sig := list{a, b, c}
sdl: 36 output := sig
sdl: 37 END :: func:sign
sdl: 38
sdl: 39
sdl: 40 BEGIN :: func:verify
sdl: 41 input := list{pk, g, M, sig}
sdl: 42 sig := expand{a, b, c}
sdl: 43 pk := expand{X, Y}
sdl: 44 m := H(M,ZR)
sdl: 45 BEGIN :: if
sdl: 46 if {{e(a,Y) == e(g,b)} and {(e(X,a) * (e(X,b)^m)) == e(g,c)}}
sdl: 47 output := True
sdl: 48 else
sdl: 49 output := False
sdl: 50 END :: if
sdl: 51 END :: func:verify
sdl: 52
name is cl04
setting is symmetric
reducing size of 'signature'
10 : G1 :=> g := random(G1) , loop :=> False
Each: if {{e(a,Y) == e(g,b)} and {(e(X,a) * (e(X,b)^m)) == e(g,c)}}
<=== Setup Graph ===>
digraph setup {
}

<=== Setup Graph ===>
<=== Keygen Graph ===>
digraph keygen {
g -> X
g -> Y
}

<=== Keygen Graph ===>
<=== Sign Graph ===>
digraph sign {
g -> a
a -> b
a -> c
}

<=== Sign Graph ===>
<=== Verify Graph ===>
digraph verify {
a -> "P1[0]"
Y -> "P1[1]"
g -> "P2[0]"
b -> "P2[1]"
X -> "P3[0]"
a -> "P3[1]"
X -> "P4[0]"
b -> "P4[1]"
g -> "P5[0]"
c -> "P5[1]"
}

<=== Verify Graph ===>
<=== Scheme Graph ===>
digraph cl04 {
g -> Y
a -> c
a -> b
X -> "P3[0]"
g -> "P5[0]"
a -> "P1[0]"
a -> "P3[1]"
X -> "P4[0]"
Y -> "P1[1]"
b -> "P4[1]"
g -> a
b -> "P2[1]"
g -> X
g -> "P2[0]"
c -> "P5[1]"
}

<=== Scheme Graph ===>

<=== Assumption Graph ===>
digraph assumption {
g -> Y
g -> X
g
}

<=== Assumption Graph ===>
<=== Reduction Graph ===>
digraph reduction {
g -> Y
a -> c
a -> b
g
g -> a
g -> X
}

<=== Reduction Graph ===>
<=== Merged Graph ===>
digraph merged {
g -> Y
a -> c
a -> b
X -> "P3[0]"
g -> "P5[0]"
a -> "P1[0]"
a -> "P3[1]"
g
X -> "P4[0]"
Y -> "P1[1]"
b -> "P4[1]"
g -> a
b -> "P2[1]"
g -> X
g -> "P2[0]"
c -> "P5[1]"
}

<=== Merged Graph ===>
pair vars LHS: ['a', 'g', 'X', 'X', 'g']
pair vars RHS: ['Y', 'b', 'a', 'b', 'c']
list of gens : ['g']
constraintList: []
pruned varList: ['a', 'b', 'c']
<===== Instantiate Z3 solver =====>
Traceback (most recent call last):
File "runAutoGroup.py", line 891, in
configAutoGroup(dest_path, sdl_file, config_file, output_file, verbose, benchmarkOpt, estimateSize, short_option, run_auto_group)
File "runAutoGroup.py", line 871, in configAutoGroup
(outfile_scheme, outfile_assump) = runAutoGroup(sdl_file, cm, options, verbose, assumptionData, reductionData)
File "/Users/watsonladd/ext-repos/auto-tools/auto_group/src/convertToAsymmetric.py", line 2461, in runAutoGroup
fileSuffix, resultDict = searchForSolution(info, short, constraintList, txor, varTypes, config, generators)
File "/Users/watsonladd/ext-repos/auto-tools/auto_group/src/convertToAsymmetric.py", line 898, in searchForSolution
pkMapMin, pkListMin, assumpMapMin, assumpList, xorVarMap)
File "/Users/watsonladd/ext-repos/auto-tools/auto_group/src/convertToAsymmetric.py", line 625, in instantiateZ3Solver
(result, satisfiable) = solveUsingSMT(info, options, shortOpt, timeOpt)
File "/Users/watsonladd/ext-repos/auto-tools/auto_group/src/solver.py", line 729, in solveUsingSMT
(mySolver, Conditions, Values, EntireSet) = getNewSolver(clauses, Z3vars, hard_constraints) # add
File "/Users/watsonladd/ext-repos/auto-tools/auto_group/src/solver.py", line 655, in getNewSolver
if Z3vars.get(x) and Z3vars.get(y):
File "/usr/local/lib/python3.7/site-packages/z3/z3.py", line 343, in bool
raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.")
z3.z3types.Z3Exception: Symbolic expressions cannot be cast to concrete Boolean values.`

Sadly installing trunk z3 didn't work with python3 on my machine, but I'm a bit surprised this would have changed. Let me know what information would help in digging into this more.