Skip to content

Instantly share code, notes, and snippets.

@taegyunkim

taegyunkim/flowlets_pred_raw_stateless_alu_5_4_codegen_iteration_2_output.txt

Created May 16, 2019 15:28
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save taegyunkim/19d2c7d02fbe82db123eafab228170b7 to your computer and use it in GitHub Desktop.
Save taegyunkim/19d2c7d02fbe82db123eafab228170b7 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
flowlets_pred_raw_stateless_alu_5_4_codegen_iteration_2_output.txt
SKETCH version 1.7.5
Benchmark = flowlets_pred_raw_stateless_alu_5_4_codegen_iteration_2.sk
[1557948961.7150 - DEBUG] Running stage 'parse' -- Parse the program from a file
[1557948962.1240 - DEBUG] Running stage 'preproc' -- Preprocessing (used for all further transformations)
[1557948962.4090 - DEBUG] Running stage SpmdLowLevelCStage
[1557948962.4130 - DEBUG] Running visitor FlattenStmtBlocks2
[1557948962.4190 - DEBUG] Running visitor SplitAssignFromVarDef
[1557948962.4240 - DEBUG] Running visitor EliminateComplexForLoops
[1557948962.4300 - DEBUG] Running stage 'lowering' -- Lower for SKETCH backend
[1557948962.4710 - DEBUG] Running stage 'sten' -- Stencil transformations
[SATBackend] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
[SATBackend] MAX LOOP UNROLLING = 8
[SATBackend] MAX FUNC INLINING = 5
estimated size of main__Wrapper
stmt cnt: 0
callee main : 272
[SATBackend] After prog.accept(partialEval)
[SATBackend] OFILE = null
searching for file null
searching for file /usr/local/sketch-1.7.5/sketch-frontend/cegis/src/SketchSolver/cegis
searching for file /usr/local/sketch-1.7.5/sketch-frontend/cegis
searching for file cegis/src/SketchSolver/cegis
searching for file ../sketch-backend/src/SketchSolver/cegis
searching for file ../sketch-backend/bindings/cegis
searching for file /home/taegyunk/.sketch/cegis-1.7.5
searching for file /home/taegyunk/.sketch/cegis
searching for file /home/taegyunk/.pyenv/versions/chipmunk/bin/cegis
searching for file /home/taegyunk/.pyenv/versions/chipmunk/bin/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/versions/chipmunk/bin/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/versions/chipmunk/bin/../sketch-backend/bindings/cegis
searching for file /home/taegyunk/.pyenv/libexec/cegis
searching for file /home/taegyunk/.pyenv/libexec/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/libexec/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/libexec/../sketch-backend/bindings/cegis
searching for file /home/taegyunk/.pyenv/plugins/python-build/bin/cegis
searching for file /home/taegyunk/.pyenv/plugins/python-build/bin/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/plugins/python-build/bin/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/plugins/python-build/bin/../sketch-backend/bindings/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-virtualenv/bin/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-virtualenv/bin/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-virtualenv/bin/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-virtualenv/bin/../sketch-backend/bindings/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-update/bin/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-update/bin/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-update/bin/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-update/bin/../sketch-backend/bindings/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-installer/bin/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-installer/bin/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-installer/bin/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-installer/bin/../sketch-backend/bindings/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-doctor/bin/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-doctor/bin/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-doctor/bin/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-doctor/bin/../sketch-backend/bindings/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-virtualenv/shims/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-virtualenv/shims/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-virtualenv/shims/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/plugins/pyenv-virtualenv/shims/../sketch-backend/bindings/cegis
searching for file /home/taegyunk/.pyenv/shims/cegis
searching for file /home/taegyunk/.pyenv/shims/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/shims/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/shims/../sketch-backend/bindings/cegis
searching for file /home/taegyunk/.pyenv/bin/cegis
searching for file /home/taegyunk/.pyenv/bin/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/bin/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/.pyenv/bin/../sketch-backend/bindings/cegis
searching for file /home/taegyunk/.jenv/bin/cegis
searching for file /home/taegyunk/.jenv/bin/src/SketchSolver/cegis
searching for file /home/taegyunk/.jenv/bin/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/.jenv/bin/../sketch-backend/bindings/cegis
searching for file /home/taegyunk/.cargo/bin/cegis
searching for file /home/taegyunk/.cargo/bin/src/SketchSolver/cegis
searching for file /home/taegyunk/.cargo/bin/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/.cargo/bin/../sketch-backend/bindings/cegis
searching for file /home/taegyunk/Workspace/ns-2-allinone/bin/cegis
searching for file /home/taegyunk/Workspace/ns-2-allinone/bin/src/SketchSolver/cegis
searching for file /home/taegyunk/Workspace/ns-2-allinone/bin/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/Workspace/ns-2-allinone/bin/../sketch-backend/bindings/cegis
searching for file /home/taegyunk/Workspace/ns-2-allinone/tcl8.5.10/unix/cegis
searching for file /home/taegyunk/Workspace/ns-2-allinone/tcl8.5.10/unix/src/SketchSolver/cegis
searching for file /home/taegyunk/Workspace/ns-2-allinone/tcl8.5.10/unix/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/Workspace/ns-2-allinone/tcl8.5.10/unix/../sketch-backend/bindings/cegis
searching for file /home/taegyunk/Workspace/ns-2-allinone/tk8.5.10/unix/cegis
searching for file /home/taegyunk/Workspace/ns-2-allinone/tk8.5.10/unix/src/SketchSolver/cegis
searching for file /home/taegyunk/Workspace/ns-2-allinone/tk8.5.10/unix/../sketch-backend/src/SketchSolver/cegis
searching for file /home/taegyunk/Workspace/ns-2-allinone/tk8.5.10/unix/../sketch-backend/bindings/cegis
searching for file /usr/local/bin/cegis
searching for file /usr/local/bin/src/SketchSolver/cegis
searching for file /usr/local/bin/../sketch-backend/src/SketchSolver/cegis
searching for file /usr/local/bin/../sketch-backend/bindings/cegis
searching for file /usr/local/sbin/cegis
searching for file /usr/local/sbin/src/SketchSolver/cegis
searching for file /usr/local/sbin/../sketch-backend/src/SketchSolver/cegis
searching for file /usr/local/sbin/../sketch-backend/bindings/cegis
searching for file /usr/local/sketch-1.7.5/sketch-frontend/cegis
searching for file /usr/local/sketch-1.7.5/sketch-frontend/src/SketchSolver/cegis
searching for file /usr/local/sketch-1.7.5/sketch-frontend/../sketch-backend/src/SketchSolver/cegis
resolved cegis to path /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis
[1557948962.6760 - DEBUG] executing /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis --bnd-inbits 2 --boundmode CALLNAME --verbosity 12 --print-version --seed 1 -simiters 4 -nativeints --assumebcheck --bnd-inline-amnt 5 -angelictupledepth 1 -srctupledepth 2 -sprandbias 1 -o /home/taegyunk/.sketch/tmp/flowlets_pred_raw_stateless_alu_5_4_codegen_iteration_2.sk/solution0-0 /home/taegyunk/.sketch/tmp/flowlets_pred_raw_stateless_alu_5_4_codegen_iteration_2.sk/input0.tmp
[SATBackend] Launching: /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis --bnd-inbits 2 --boundmode CALLNAME --verbosity 12 --print-version --seed 1 -simiters 4 -nativeints --assumebcheck --bnd-inline-amnt 5 -angelictupledepth 1 -srctupledepth 2 -sprandbias 1 -o /home/taegyunk/.sketch/tmp/flowlets_pred_raw_stateless_alu_5_4_codegen_iteration_2.sk/solution0-0 /home/taegyunk/.sketch/tmp/flowlets_pred_raw_stateless_alu_5_4_codegen_iteration_2.sk/input0.tmp
starting command line: [/usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis, --bnd-inbits, 2, --boundmode, CALLNAME, --verbosity, 12, --print-version, --seed, 1, -simiters, 4, -nativeints, --assumebcheck, --bnd-inline-amnt, 5, -angelictupledepth, 1, -srctupledepth, 2, -sprandbias, 1, -o, /home/taegyunk/.sketch/tmp/flowlets_pred_raw_stateless_alu_5_4_codegen_iteration_2.sk/solution0-0, /home/taegyunk/.sketch/tmp/flowlets_pred_raw_stateless_alu_5_4_codegen_iteration_2.sk/input0.tmp]
Overriding inputs with 2
boundmode = CALLNAME
NATIVE INTS ONassuming bounds checks
SOLVER RAND SEED = 1
optimization level = 6
Reading SKETCH Program in File /home/taegyunk/.sketch/tmp/flowlets_pred_raw_stateless_alu_5_4_codegen_iteration_2.sk/input0.tmp
CREATING main__Wrapper
size = 8
after ba size = 8
CREATING main__WrapperNospec
size = 6
after ba size = 6
CREATING main
size = 278
after ba size = 278
CREATING pipeline
size = 548
after ba size = 548
CREATING program
size = 13
after ba size = 13
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_0
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_1
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_2
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_3
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_0_0_0
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_0_0_1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_0_1_0
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_0_1_1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_0
size = 30
after ba size = 30
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_1
size = 30
after ba size = 30
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_0_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_0_1
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_0_2
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_0_3
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_0
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_1
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_2
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_3
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_1_0_0
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_1_0_1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_1_1_0
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_1_1_1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_0
size = 30
after ba size = 30
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_1
size = 30
after ba size = 30
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_1_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_1_1
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_1_2
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_1_3
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_0
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_1
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_2
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_3
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_2_0_0
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_2_0_1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_2_1_0
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_2_1_1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_0
size = 30
after ba size = 30
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_1
size = 30
after ba size = 30
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_2_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_2_1
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_2_2
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_2_3
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_0
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_1
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_2
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_3
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_3_0_0
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_3_0_1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_3_1_0
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_3_1_1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_0
size = 30
after ba size = 30
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_1
size = 30
after ba size = 30
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_3_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_3_1
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_3_2
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_3_3
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_0
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_1
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_2
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_3
size = 169
after ba size = 169
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_4_0_0
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_4_0_1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_4_1_0
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_operand_mux_4_1_1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_0
size = 30
after ba size = 30
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_1
size = 30
after ba size = 30
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_4_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_4_1
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_4_2
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_output_mux_phv_4_3
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_0_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_0_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_0_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_1_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_1_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_1_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_2_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_2_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_2_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_3_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_3_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_0_3_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_0_Opt_0
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_0_C_0
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_0_Mux3_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_0_rel_op_0
size = 33
after ba size = 33
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_0_Opt_1
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_0_C_1
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_0_Mux3_1
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_1_Opt_0
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_1_C_0
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_1_Mux3_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_1_rel_op_0
size = 33
after ba size = 33
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_1_Opt_1
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_1_C_1
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_0_1_Mux3_1
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_0_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_0_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_0_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_1_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_1_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_1_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_2_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_2_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_2_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_3_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_3_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_1_3_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_0_Opt_0
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_0_C_0
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_0_Mux3_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_0_rel_op_0
size = 33
after ba size = 33
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_0_Opt_1
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_0_C_1
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_0_Mux3_1
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_1_Opt_0
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_1_C_0
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_1_Mux3_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_1_rel_op_0
size = 33
after ba size = 33
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_1_Opt_1
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_1_C_1
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_1_1_Mux3_1
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_0_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_0_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_0_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_1_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_1_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_1_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_2_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_2_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_2_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_3_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_3_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_2_3_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_0_Opt_0
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_0_C_0
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_0_Mux3_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_0_rel_op_0
size = 33
after ba size = 33
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_0_Opt_1
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_0_C_1
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_0_Mux3_1
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_1_Opt_0
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_1_C_0
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_1_Mux3_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_1_rel_op_0
size = 33
after ba size = 33
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_1_Opt_1
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_1_C_1
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_2_1_Mux3_1
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_0_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_0_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_0_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_1_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_1_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_1_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_2_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_2_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_2_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_3_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_3_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_3_3_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_0_Opt_0
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_0_C_0
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_0_Mux3_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_0_rel_op_0
size = 33
after ba size = 33
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_0_Opt_1
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_0_C_1
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_0_Mux3_1
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_1_Opt_0
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_1_C_0
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_1_Mux3_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_1_rel_op_0
size = 33
after ba size = 33
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_1_Opt_1
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_1_C_1
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_3_1_Mux3_1
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_0_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_0_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_0_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_1_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_1_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_1_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_2_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_2_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_2_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_3_mux1
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_3_mux2
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateless_alu_4_3_mux3
size = 27
after ba size = 27
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_0_Opt_0
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_0_C_0
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_0_Mux3_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_0_rel_op_0
size = 33
after ba size = 33
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_0_Opt_1
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_0_C_1
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_0_Mux3_1
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_1_Opt_0
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_1_C_0
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_1_Mux3_0
size = 20
after ba size = 20
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_1_rel_op_0
size = 33
after ba size = 33
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_1_Opt_1
size = 10
after ba size = 10
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_1_C_1
size = 3
after ba size = 3
CREATING flowlets_pred_raw_stateless_alu_5_4_stateful_alu_4_1_Mux3_1
size = 20
after ba size = 20
* before EVERYTHING: main__WrapperNospec::SPEC nodes = 6 main__Wrapper::SKETCH nodes = 8
INBITS = 2
CBITS = 5
input_ints = 6 input_bits = 0
Inlining amount = 5
Inlining functions in the sketch.
inlined 1 new size =263
inlined 18 new size =2193
inlined 1530 new size =17048
inlined 190 new size =17618
inlined 0 new size =17618
END OF STEP 0
Inlining functions in the spec.
inlined 0 new size =6
END OF STEP 0
Bailing out
after Creating Miter: Problem nodes = 17618
* Final Problem size: Problem nodes = 17618
# OF CONTROLS: 220
control_ints = 190 control_bits = 30
inputSize = 12 ctrlSize = 470
Random seeds = 1
!+ 00000001000000001011010000000000000001000000100100000110001000101000001000000100011011000011110100000000000001110100001010000000000100000001101000011010100000000111000101100100000110010000000000010010110000011011000110000010100000000100011001000110000000001110001100100111100010000000100001000100001101101001000111001000000100000100100100101100100111100000100000100001100100010010010000100000100010011011001101000100001010100000000100110100110011100110000000101000000001
!+ H__0:0
H__1:0
H__3:8
H__5:0
H__6:0
H__8:8
H__10:3
H__11:2
H__13:0
H__15:0
H__16:0
H__18:0
H__34:2
H__35:0
H__37:16
H__39:0
H__40:1
H__42:16
H__44:1
H__45:0
H__47:17
H__49:2
H__50:0
H__52:8
H__68:0
H__69:0
H__71:2
H__73:3
H__74:2
H__76:1
H__78:3
H__79:3
H__81:2
H__83:0
H__84:0
H__86:0
H__102:2
H__103:3
H__105:2
H__107:2
H__108:2
H__110:0
H__112:0
H__113:0
H__115:2
H__117:0
H__118:0
H__120:11
H__136:0
H__137:2
H__139:21
H__141:0
H__142:0
H__144:16
H__146:3
H__147:0
H__149:26
H__151:0
H__152:1
H__154:16
H__218:1
H__216:0
H__214:0
H__212:1
H__210:0
H__219:0
H__217:0
H__215:0
H__213:0
H__211:0
H__26:0
H__33:0
H__60:2
H__67:0
H__94:1
H__101:3
H__128:0
H__135:0
H__162:2
H__169:1
H__20:3
H__171:0
H__24:2
H__170:1
H__22:0
H__21:0
H__25:2
H__23:0
H__54:1
H__175:0
H__191:0
H__9:0
H__7:2
H__192:0
H__14:2
H__12:1
H__193:2
H__19:0
H__17:2
H__190:1
H__4:0
H__2:0
H__58:0
H__174:0
H__56:1
H__55:3
H__59:0
H__57:0
H__88:3
H__179:0
H__195:1
H__27:2
H__173:3
H__31:1
H__172:0
H__29:1
H__28:0
H__32:0
H__30:0
H__43:0
H__41:1
H__196:0
H__48:2
H__46:0
H__197:2
H__53:0
H__51:0
H__194:3
H__38:2
H__36:1
H__92:1
H__178:2
H__90:0
H__89:0
H__93:3
H__91:1
H__122:0
H__183:1
H__199:0
H__61:0
H__177:2
H__65:0
H__176:0
H__63:0
H__62:1
H__66:2
H__64:0
H__77:2
H__75:0
H__200:1
H__82:3
H__80:0
H__201:1
H__87:2
H__85:3
H__198:1
H__72:0
H__70:0
H__126:1
H__182:0
H__124:0
H__123:2
H__127:0
H__125:0
H__156:2
H__187:1
H__203:2
H__95:0
H__181:2
H__99:0
H__180:1
H__97:0
H__96:1
H__100:0
H__98:0
H__111:1
H__109:0
H__204:0
H__116:1
H__114:0
H__205:1
H__121:2
H__119:1
H__202:3
H__106:0
H__104:3
H__160:2
H__186:0
H__158:0
H__157:1
H__161:0
H__159:0
H__129:1
H__185:1
H__133:1
H__184:0
H__131:0
H__130:0
H__134:0
H__132:1
H__163:0
H__189:3
H__167:2
H__188:0
H__165:1
H__164:1
H__168:2
H__166:1
H__206:1
H__140:2
H__138:1
H__207:0
H__145:0
H__143:0
H__208:1
H__150:1
H__148:0
H__209:0
H__155:0
H__153:2
BEG CHECK
* After optims it became = 8 was 17618
Assert at flowlet..tion_2.sk:3261 (0)
Simulation found a cex by random testing: 0 ms
END CHECK
******** 0 ftime= 0 ctime= 0.013
!% 001001000001
!% pkt_0_6_6_0:0
pkt_1_7_7_0:1
pkt_2_8_8_0:2
pkt_3_9_9_0:0
state_group_0_state_0_a_a_0:0
state_group_1_state_0_b_b_0:2
BEG FIND
Level 1 intsize = 2
* After optims it became = 17587 was 17618
* After all optims it became = 17587
finder hits = 161236 bstoreObjs=188298 sstorePages=351
hitcount 0 142125 7
hitcount 1 5892 7
hitcount 2 52 4
hitcount 3 15037 9
hitcount 4 21682 8
hitcount 5 412 8
hitcount 6 2382 7
hitcount 7 343 6
hitcount 8 21 2
hitcount 9 176 8
hitcount 11 16 8
hitcount 13 36 7
hitcount 14 72 8
hitcount 15 4 5
hitcount 20 24 7
hitcount 22 8 0
hitcount 31 12 6
hitcount 39 4 7
bucketsPerDepth 11 14
bucketsPerDepth 12 81
bucketsPerDepth 13 230
bucketsPerDepth 14 246
bucketsPerDepth 15 195
bucketsPerDepth 16 118
bucketsPerDepth 17 69
bucketsPerDepth 18 43
bucketsPerDepth 19 19
bucketsPerDepth 20 6
bucketsPerDepth 21 3
* TIME TO ADD INPUT : 999.477 ms
DECISIONS START = 0
f# %assign: 0 clauses: 1140273 learn: 454918 restart: 20 decision: 1728036 propagated: 1475390041
END FIND
!+ 10111010011110011000010111000011100001111100010110111011110010011011000001011111010010001100011010011110111010100111011111100111011000011111111011011000010010111011111111011011000000001001000000101111010010011101000110010001000101011001101111101111101000110001000111011010001001010011010111000001100111111011001000111101011010100000000100010011110110100011101100110001000101101111010101001001110101010111000001000000101001101000000011011001000010011011010100011001110011
!+ H__0:1
H__1:3
H__3:5
H__5:3
H__6:3
H__8:12
H__10:0
H__11:2
H__13:14
H__15:0
H__16:2
H__18:3
H__34:2
H__35:3
H__37:3
H__39:1
H__40:3
H__42:14
H__44:3
H__45:3
H__47:4
H__49:3
H__50:2
H__52:1
H__68:2
H__69:2
H__71:15
H__73:1
H__74:2
H__76:24
H__78:0
H__79:2
H__81:5
H__83:3
H__84:3
H__86:14
H__102:1
H__103:1
H__105:14
H__107:3
H__108:3
H__110:19
H__112:3
H__113:2
H__115:1
H__117:3
H__118:3
H__120:15
H__136:3
H__137:2
H__139:1
H__141:1
H__142:2
H__144:14
H__146:3
H__147:3
H__149:15
H__151:3
H__152:2
H__154:1
H__218:0
H__216:0
H__214:0
H__212:0
H__210:1
H__219:0
H__217:0
H__215:1
H__213:0
H__211:0
H__26:0
H__33:0
H__60:1
H__67:3
H__94:3
H__101:2
H__128:0
H__135:1
H__162:2
H__169:3
H__20:2
H__171:0
H__24:2
H__170:1
H__22:0
H__21:1
H__25:0
H__23:1
H__54:0
H__175:2
H__191:2
H__9:2
H__7:1
H__192:2
H__14:1
H__12:3
H__193:3
H__19:1
H__17:3
H__190:3
H__4:1
H__2:1
H__58:0
H__174:3
H__56:0
H__55:0
H__59:1
H__57:0
H__88:2
H__179:3
H__195:2
H__27:1
H__173:1
H__31:0
H__172:1
H__29:0
H__28:1
H__32:1
H__30:0
H__43:3
H__41:2
H__196:2
H__48:3
H__46:0
H__197:0
H__53:2
H__51:1
H__194:2
H__38:3
H__36:3
H__92:1
H__178:3
H__90:0
H__89:2
H__93:0
H__91:0
H__122:3
H__183:3
H__199:2
H__61:2
H__177:1
H__65:1
H__176:1
H__63:0
H__62:0
H__66:0
H__64:0
H__77:2
H__75:0
H__200:2
H__82:0
H__80:3
H__201:3
H__87:2
H__85:1
H__198:1
H__72:0
H__70:3
H__126:1
H__182:3
H__124:0
H__123:2
H__127:1
H__125:0
H__156:2
H__187:0
H__203:2
H__95:2
H__181:1
H__99:3
H__180:3
H__97:0
H__96:1
H__100:1
H__98:1
H__111:0
H__109:1
H__204:2
H__116:3
H__114:2
H__205:2
H__121:2
H__119:2
H__202:3
H__106:0
H__104:0
H__160:2
H__186:0
H__158:0
H__157:0
H__161:2
H__159:0
H__129:1
H__185:2
H__133:1
H__184:1
H__131:0
H__130:0
H__134:0
H__132:0
H__163:3
H__189:2
H__167:1
H__188:2
H__165:0
H__164:0
H__168:2
H__166:0
H__206:2
H__140:1
H__138:3
H__207:2
H__145:2
H__143:0
H__208:2
H__150:1
H__148:2
H__209:3
H__155:0
H__153:3
BEG CHECK
* After optims it became = 48 was 17618
Assert at flowlet..tion_2.sk:4066 (1)
Simulation found a cex by random testing: 0 ms
END CHECK
******** 1 ftime= 311000 ctime= 0.021
!% 000001100100
!% pkt_0_6_6_0:0
pkt_1_7_7_0:0
pkt_2_8_8_0:2
pkt_3_9_9_0:1
state_group_0_state_0_a_a_0:2
state_group_1_state_0_b_b_0:0
BEG FIND
Level 1 intsize = 2
* After optims it became = 17603 was 17618
* After all optims it became = 17603
finder hits = 330387 bstoreObjs=362768 sstorePages=727
hitcount 0 266299 8
hitcount 1 17799 8
hitcount 2 88 6
hitcount 3 29508 10
hitcount 4 42244 9
hitcount 5 152 9
hitcount 6 1576 8
hitcount 7 1760 9
hitcount 8 1324 7
hitcount 9 1564 8
hitcount 10 20 0
hitcount 11 8 7
hitcount 13 58 7
hitcount 14 136 9
hitcount 15 82 4
hitcount 16 26 6
hitcount 17 20 3
hitcount 19 24 7
hitcount 26 24 7
hitcount 29 32 8
hitcount 30 8 0
hitcount 31 12 6
hitcount 39 4 7
bucketsPerDepth 13 1
bucketsPerDepth 14 48
bucketsPerDepth 15 152
bucketsPerDepth 16 249
bucketsPerDepth 17 185
bucketsPerDepth 18 179
bucketsPerDepth 19 104
bucketsPerDepth 20 64
bucketsPerDepth 21 29
bucketsPerDepth 22 9
bucketsPerDepth 23 2
bucketsPerDepth 24 2
* TIME TO ADD INPUT : 999.597 ms
DECISIONS START = 1728036
f# %assign: 0 clauses: 2214606 learn: 672532 restart: 38 decision: 2209803 propagated: 2879900852
END FIND
!+ 10100111010111100000010111000101100001111000011001000001011111010101000010010010010111111000011010010010111010100111010111111011011000000111111000101000001001000011111111010010111000001100000000010011010000011101000110010001000101011001100011101111101100110001000111011010001001010011010101100101110111111011001000111101011010100110101011010011110100110011101100110001000101101000010101001001010101010111100001100000101010101000000011110001110011011011010100011011110000
!+ H__0:1
H__1:1
H__3:14
H__5:1
H__6:3
H__8:3
H__10:0
H__11:2
H__13:14
H__15:0
H__16:1
H__18:3
H__34:2
H__35:3
H__37:1
H__39:3
H__40:0
H__42:1
H__44:2
H__45:2
H__47:15
H__49:1
H__50:1
H__52:1
H__68:1
H__69:2
H__71:4
H__73:1
H__74:3
H__76:15
H__78:0
H__79:2
H__81:5
H__83:1
H__84:2
H__86:14
H__102:1
H__103:1
H__105:14
H__107:1
H__108:3
H__110:15
H__112:3
H__113:2
H__115:1
H__117:0
H__118:3
H__120:15
H__136:0
H__137:1
H__139:1
H__141:2
H__142:0
H__144:1
H__146:3
H__147:3
H__149:15
H__151:1
H__152:2
H__154:14
H__218:0
H__216:0
H__214:0
H__212:0
H__210:1
H__219:1
H__217:0
H__215:0
H__213:0
H__211:0
H__26:0
H__33:0
H__60:2
H__67:0
H__94:3
H__101:2
H__128:0
H__135:0
H__162:2
H__169:3
H__20:2
H__171:0
H__24:2
H__170:1
H__22:0
H__21:1
H__25:0
H__23:1
H__54:0
H__175:2
H__191:2
H__9:2
H__7:1
H__192:2
H__14:1
H__12:0
H__193:3
H__19:1
H__17:3
H__190:3
H__4:1
H__2:3
H__58:0
H__174:3
H__56:0
H__55:0
H__59:1
H__57:0
H__88:2
H__179:3
H__195:2
H__27:1
H__173:1
H__31:0
H__172:1
H__29:0
H__28:1
H__32:1
H__30:0
H__43:3
H__41:2
H__196:2
H__48:2
H__46:1
H__197:2
H__53:2
H__51:3
H__194:2
H__38:3
H__36:3
H__92:1
H__178:3
H__90:0
H__89:2
H__93:0
H__91:0
H__122:3
H__183:3
H__199:2
H__61:2
H__177:1
H__65:1
H__176:1
H__63:0
H__62:3
H__66:2
H__64:0
H__77:1
H__75:3
H__200:2
H__82:0
H__80:3
H__201:3
H__87:2
H__85:0
H__198:3
H__72:0
H__70:3
H__126:1
H__182:3
H__124:0
H__123:2
H__127:1
H__125:0
H__156:2
H__187:0
H__203:2
H__95:2
H__181:1
H__99:1
H__180:0
H__97:0
H__96:1
H__100:1
H__98:1
H__111:0
H__109:1
H__204:2
H__116:2
H__114:2
H__205:2
H__121:2
H__119:2
H__202:3
H__106:1
H__104:0
H__160:2
H__186:1
H__158:0
H__157:0
H__161:2
H__159:0
H__129:1
H__185:1
H__133:1
H__184:1
H__131:0
H__130:0
H__134:0
H__132:0
H__163:3
H__189:3
H__167:0
H__188:2
H__165:1
H__164:1
H__168:2
H__166:1
H__206:2
H__140:1
H__138:3
H__207:2
H__145:2
H__143:0
H__208:2
H__150:1
H__148:3
H__209:3
H__155:0
H__153:0
BEG CHECK
* After optims it became = 51 was 17618
Assert at flowlet..tion_2.sk:4064 (1)
Simulation found a cex by random testing: 0 ms
END CHECK
******** 2 ftime= 441000 ctime= 0.019
!% 010001001000
!% pkt_0_6_6_0:2
pkt_1_7_7_0:0
pkt_2_8_8_0:2
pkt_3_9_9_0:0
state_group_0_state_0_a_a_0:1
state_group_1_state_0_b_b_0:0
BEG FIND
Level 1 intsize = 2
* After optims it became = 17584 was 17618
* After all optims it became = 17584
finder hits = 582710 bstoreObjs=140309 sstorePages=241
hitcount 1 48996 5
hitcount 2 8791 5
hitcount 3 17541 5
hitcount 4 20344 5
hitcount 5 1774 5
hitcount 6 1140 5
hitcount 7 14761 5
hitcount 8 4 6
hitcount 9 22144 5
hitcount 10 1236 5
hitcount 11 1440 5
hitcount 12 20 5
hitcount 13 200 5
hitcount 14 1266 5
hitcount 15 124 5
hitcount 19 182 5
hitcount 20 22 5
hitcount 21 24 5
hitcount 22 8 5
hitcount 23 66 5
hitcount 24 22 5
hitcount 25 8 5
hitcount 26 12 5
hitcount 29 104 5
hitcount 31 12 4
hitcount 32 24 5
hitcount 36 8 5
hitcount 39 4 6
hitcount 44 32 5
bucketsPerDepth 6 237
bucketsPerDepth 7 787
* TIME TO ADD INPUT : 999.515 ms
DECISIONS START = 2209803
f# %assign: 0 clauses: 2844296 learn: 1201224 restart: 58 decision: 3262474 propagated: 9922158976
END FIND
!+ 00111111000101100010010111000011100010011000001111000001010111010101101010010010000110111000011010010010111010100111010111111011011000000111111000101000001001000011111111010100111000001100000100010011010101011101000100010001001001011001101011101100101100100001000111011000001000110011100101000101100100011011001000111101011010100110101010010011110101110011101100110001000101101110010101000101110101010111110010100000101010101000000011110001110011010010010100011011110000
!+ H__0:0
H__1:3
H__3:15
H__5:0
H__6:1
H__8:3
H__10:1
H__11:2
H__13:14
H__15:0
H__16:2
H__18:3
H__34:1
H__35:2
H__37:1
H__39:2
H__40:3
H__42:1
H__44:2
H__45:2
H__47:14
H__49:1
H__50:1
H__52:11
H__68:1
H__69:2
H__71:4
H__73:0
H__74:3
H__76:14
H__78:0
H__79:2
H__81:5
H__83:1
H__84:2
H__86:14
H__102:1
H__103:1
H__105:14
H__107:1
H__108:3
H__110:15
H__112:3
H__113:2
H__115:1
H__117:0
H__118:3
H__120:15
H__136:0
H__137:1
H__139:1
H__141:2
H__142:0
H__144:1
H__146:3
H__147:3
H__149:15
H__151:1
H__152:1
H__154:14
H__218:0
H__216:0
H__214:0
H__212:0
H__210:1
H__219:1
H__217:0
H__215:0
H__213:0
H__211:0
H__26:2
H__33:0
H__60:2
H__67:0
H__94:3
H__101:2
H__128:2
H__135:2
H__162:2
H__169:3
H__20:2
H__171:0
H__24:2
H__170:0
H__22:0
H__21:1
H__25:0
H__23:1
H__54:0
H__175:1
H__191:2
H__9:2
H__7:1
H__192:2
H__14:1
H__12:1
H__193:3
H__19:1
H__17:3
H__190:0
H__4:1
H__2:3
H__58:0
H__174:1
H__56:0
H__55:0
H__59:1
H__57:0
H__88:2
H__179:3
H__195:2
H__27:1
H__173:0
H__31:0
H__172:1
H__29:0
H__28:2
H__32:1
H__30:0
H__43:3
H__41:1
H__196:2
H__48:2
H__46:0
H__197:2
H__53:2
H__51:1
H__194:2
H__38:0
H__36:2
H__92:1
H__178:3
H__90:0
H__89:2
H__93:0
H__91:0
H__122:3
H__183:3
H__199:2
H__61:2
H__177:1
H__65:1
H__176:1
H__63:0
H__62:3
H__66:2
H__64:0
H__77:1
H__75:1
H__200:2
H__82:0
H__80:3
H__201:3
H__87:2
H__85:2
H__198:3
H__72:0
H__70:3
H__126:1
H__182:3
H__124:0
H__123:2
H__127:1
H__125:0
H__156:2
H__187:0
H__203:2
H__95:2
H__181:1
H__99:3
H__180:1
H__97:0
H__96:1
H__100:1
H__98:1
H__111:0
H__109:2
H__204:2
H__116:3
H__114:2
H__205:2
H__121:2
H__119:2
H__202:3
H__106:3
H__104:0
H__160:1
H__186:1
H__158:0
H__157:0
H__161:2
H__159:0
H__129:1
H__185:1
H__133:1
H__184:1
H__131:0
H__130:0
H__134:0
H__132:0
H__163:3
H__189:3
H__167:0
H__188:2
H__165:1
H__164:1
H__168:2
H__166:1
H__206:2
H__140:0
H__138:1
H__207:2
H__145:2
H__143:0
H__208:2
H__150:1
H__148:3
H__209:3
H__155:0
H__153:0
BEG CHECK
* After optims it became = 51 was 17618
Assert at flowlet..tion_2.sk:4066 (1)
Simulation found a cex by random testing: 0 ms
END CHECK
******** 3 ftime= 2.398e+06 ctime= 0.018
!% 000010000010
!% pkt_0_6_6_0:0
pkt_1_7_7_0:0
pkt_2_8_8_0:1
pkt_3_9_9_0:0
state_group_0_state_0_a_a_0:0
state_group_1_state_0_b_b_0:1
BEG FIND
Level 1 intsize = 2
* After optims it became = 17584 was 17618
* After all optims it became = 17584
finder hits = 829621 bstoreObjs=235802 sstorePages=518
hitcount 0 93962 7
hitcount 1 11937 5
hitcount 2 38183 5
hitcount 3 22905 5
hitcount 4 20340 5
hitcount 5 3874 5
hitcount 6 1024 5
hitcount 7 2597 5
hitcount 8 392 5
hitcount 9 152 5
hitcount 11 13738 5
hitcount 12 1224 5
hitcount 13 28 5
hitcount 14 21936 5
hitcount 15 1448 5
hitcount 16 12 5
hitcount 17 12 4
hitcount 19 1226 5
hitcount 20 172 4
hitcount 23 116 5
hitcount 25 4 4
hitcount 27 22 5
hitcount 28 16 5
hitcount 29 178 5
hitcount 30 8 5
hitcount 31 74 5
hitcount 32 26 5
hitcount 33 4 6
hitcount 34 8 5
hitcount 35 12 5
hitcount 38 24 5
hitcount 39 28 5
hitcount 43 4 5
hitcount 44 84 5
hitcount 59 32 5
bucketsPerDepth 9 51
bucketsPerDepth 10 490
bucketsPerDepth 11 387
bucketsPerDepth 12 83
bucketsPerDepth 13 12
bucketsPerDepth 14 1
* TIME TO ADD INPUT : 999.387 ms
DECISIONS START = 3262474
f# %assign: 0 clauses: 3596562 learn: 1802876 restart: 78 decision: 4384287 propagated: 20065773676
END FIND
!+ 00111111000101100010010010000011100001110010001101000001010111011111010011110010000011100010011010010010111010011100010111111011011000000011100000101000001001000011111111010100111000001100000100011111010001011101000100010001001101011001001011101100101100100001000100011000001000110010100110000100100100010100001000110001011110110110100010010010110101110000100101010001000101111011010101000101100101011111110000100000101000100000000011110011100011011010011100011011111000
!+ H__0:0
H__1:3
H__3:15
H__5:0
H__6:1
H__8:3
H__10:1
H__11:2
H__13:4
H__15:0
H__16:2
H__18:3
H__34:2
H__35:3
H__37:4
H__39:2
H__40:1
H__42:1
H__44:2
H__45:2
H__47:14
H__49:3
H__50:3
H__52:5
H__68:3
H__69:3
H__71:4
H__73:0
H__74:2
H__76:3
H__78:1
H__79:2
H__81:5
H__83:1
H__84:2
H__86:14
H__102:1
H__103:2
H__105:3
H__107:1
H__108:3
H__110:15
H__112:3
H__113:2
H__115:1
H__117:0
H__118:2
H__120:3
H__136:0
H__137:1
H__139:1
H__141:2
H__142:0
H__144:1
H__146:3
H__147:3
H__149:15
H__151:1
H__152:1
H__154:14
H__218:0
H__216:0
H__214:0
H__212:0
H__210:1
H__219:1
H__217:0
H__215:0
H__213:0
H__211:0
H__26:2
H__33:0
H__60:2
H__67:3
H__94:3
H__101:2
H__128:0
H__135:2
H__162:2
H__169:3
H__20:2
H__171:0
H__24:2
H__170:0
H__22:0
H__21:1
H__25:0
H__23:1
H__54:0
H__175:3
H__191:2
H__9:2
H__7:1
H__192:2
H__14:0
H__12:1
H__193:3
H__19:1
H__17:3
H__190:0
H__4:1
H__2:3
H__58:0
H__174:1
H__56:0
H__55:0
H__59:1
H__57:0
H__88:2
H__179:0
H__195:2
H__27:1
H__173:0
H__31:0
H__172:1
H__29:0
H__28:2
H__32:1
H__30:0
H__43:1
H__41:1
H__196:2
H__48:1
H__46:0
H__197:2
H__53:0
H__51:1
H__194:2
H__38:0
H__36:2
H__92:2
H__178:0
H__90:0
H__89:2
H__93:0
H__91:0
H__122:3
H__183:0
H__199:2
H__61:2
H__177:3
H__65:1
H__176:3
H__63:0
H__62:3
H__66:2
H__64:0
H__77:0
H__75:1
H__200:2
H__82:0
H__80:1
H__201:3
H__87:2
H__85:2
H__198:3
H__72:0
H__70:0
H__126:1
H__182:2
H__124:0
H__123:1
H__127:1
H__125:0
H__156:2
H__187:0
H__203:2
H__95:2
H__181:3
H__99:1
H__180:3
H__97:0
H__96:1
H__100:1
H__98:1
H__111:0
H__109:2
H__204:2
H__116:1
H__114:2
H__205:2
H__121:2
H__119:3
H__202:3
H__106:3
H__104:0
H__160:0
H__186:1
H__158:0
H__157:0
H__161:2
H__159:0
H__129:1
H__185:0
H__133:1
H__184:0
H__131:0
H__130:0
H__134:0
H__132:0
H__163:3
H__189:3
H__167:0
H__188:3
H__165:1
H__164:0
H__168:2
H__166:1
H__206:2
H__140:1
H__138:1
H__207:2
H__145:3
H__143:0
H__208:2
H__150:1
H__148:3
H__209:3
H__155:1
H__153:0
BEG CHECK
* After optims it became = 46 was 17618
Assert at flowlet..tion_2.sk:4072 (1)
Simulation found a cex by random testing: 0 ms
END CHECK
******** 4 ftime= 4.281e+06 ctime= 0.021
!% 010010100011
!% pkt_0_6_6_0:2
pkt_1_7_7_0:0
pkt_2_8_8_0:1
pkt_3_9_9_0:1
state_group_0_state_0_a_a_0:0
state_group_1_state_0_b_b_0:3
BEG FIND
Level 1 intsize = 2
* After optims it became = 17603 was 17618
* After all optims it became = 17603
finder hits = 1103021 bstoreObjs=305816 sstorePages=710
hitcount 0 134860 8
hitcount 1 40817 7
hitcount 2 2597 5
hitcount 3 49554 5
hitcount 4 28970 5
hitcount 5 60 5
hitcount 6 1028 5
hitcount 7 5096 5
hitcount 8 128 5
hitcount 9 2250 5
hitcount 10 8 5
hitcount 11 20 5
hitcount 12 100 5
hitcount 13 28 5
hitcount 14 1264 5
hitcount 15 13634 5
hitcount 17 16 5
hitcount 18 4 4
hitcount 19 23328 5
hitcount 21 4 5
hitcount 22 8 5
hitcount 23 4 5
hitcount 24 1226 5
hitcount 25 4 4
hitcount 27 172 4
hitcount 29 4 4
hitcount 31 124 5
hitcount 34 22 5
hitcount 35 16 5
hitcount 37 8 5
hitcount 38 16 5
hitcount 39 228 5
hitcount 40 10 5
hitcount 41 16 4
hitcount 43 8 5
hitcount 44 36 5
hitcount 45 4 6
hitcount 49 28 5
hitcount 50 4 5
hitcount 59 80 5
hitcount 74 32 5
bucketsPerDepth 10 38
bucketsPerDepth 11 382
bucketsPerDepth 12 418
bucketsPerDepth 13 153
bucketsPerDepth 14 30
bucketsPerDepth 15 2
bucketsPerDepth 16 1
* TIME TO ADD INPUT : 999.379 ms
DECISIONS START = 4384287
f# %assign: 0 clauses: 4117824 learn: 2266163 restart: 100 decision: 6687104 propagated: 48497740776
END FIND
!+ 00111111000101100010010010000011100001110010001101000001010111011111010011110010000101100010101111000100111010111100011111010011011000000011000001101000001001000011111111010101010000001100000100001111010001000001000100010001101101011001001011101100101100010101000100011000001000110010100110000100100100010100001000110001010110100110100010010010111001110000100101010001000101111011010101001101010101011111101001110100101000100000000011111011000011011010010000011011110001
!+ H__0:0
H__1:3
H__3:15
H__5:0
H__6:1
H__8:3
H__10:1
H__11:2
H__13:4
H__15:0
H__16:2
H__18:3
H__34:2
H__35:3
H__37:4
H__39:2
H__40:1
H__42:1
H__44:2
H__45:2
H__47:14
H__49:3
H__50:3
H__52:5
H__68:3
H__69:3
H__71:4
H__73:0
H__74:1
H__76:3
H__78:1
H__79:1
H__81:15
H__83:0
H__84:1
H__86:14
H__102:1
H__103:3
H__105:3
H__107:3
H__108:3
H__110:5
H__112:3
H__113:2
H__115:1
H__117:0
H__118:2
H__120:1
H__136:2
H__137:1
H__139:1
H__141:2
H__142:0
H__144:1
H__146:3
H__147:3
H__149:15
H__151:1
H__152:1
H__154:5
H__218:0
H__216:0
H__214:0
H__212:0
H__210:1
H__219:1
H__217:0
H__215:0
H__213:0
H__211:0
H__26:2
H__33:0
H__60:0
H__67:3
H__94:3
H__101:2
H__128:0
H__135:2
H__162:0
H__169:0
H__20:2
H__171:0
H__24:2
H__170:0
H__22:0
H__21:1
H__25:0
H__23:1
H__54:1
H__175:3
H__191:2
H__9:2
H__7:1
H__192:2
H__14:0
H__12:1
H__193:3
H__19:1
H__17:3
H__190:0
H__4:1
H__2:3
H__58:0
H__174:2
H__56:0
H__55:1
H__59:1
H__57:0
H__88:2
H__179:0
H__195:2
H__27:1
H__173:0
H__31:0
H__172:1
H__29:0
H__28:2
H__32:1
H__30:0
H__43:1
H__41:1
H__196:2
H__48:1
H__46:0
H__197:2
H__53:0
H__51:1
H__194:2
H__38:0
H__36:2
H__92:2
H__178:0
H__90:0
H__89:2
H__93:0
H__91:0
H__122:3
H__183:0
H__199:2
H__61:2
H__177:2
H__65:1
H__176:1
H__63:0
H__62:3
H__66:2
H__64:0
H__77:0
H__75:1
H__200:2
H__82:0
H__80:1
H__201:3
H__87:1
H__85:2
H__198:3
H__72:0
H__70:0
H__126:1
H__182:2
H__124:0
H__123:1
H__127:1
H__125:0
H__156:2
H__187:0
H__203:2
H__95:2
H__181:3
H__99:1
H__180:3
H__97:0
H__96:1
H__100:1
H__98:1
H__111:0
H__109:3
H__204:2
H__116:2
H__114:2
H__205:2
H__121:2
H__119:3
H__202:3
H__106:1
H__104:1
H__160:2
H__186:3
H__158:0
H__157:1
H__161:2
H__159:0
H__129:1
H__185:0
H__133:1
H__184:0
H__131:0
H__130:0
H__134:0
H__132:0
H__163:3
H__189:3
H__167:1
H__188:3
H__165:0
H__164:0
H__168:2
H__166:1
H__206:2
H__140:1
H__138:1
H__207:2
H__145:0
H__143:0
H__208:2
H__150:1
H__148:3
H__209:3
H__155:0
H__153:2
BEG CHECK
* After optims it became = 49 was 17618
Assert at flowlet..tion_2.sk:4071 (1)
Simulation found a cex by random testing: 0 ms
END CHECK
******** 5 ftime= 1.1236e+07 ctime= 0.019
!% 000000010000
!% pkt_0_6_6_0:0
pkt_1_7_7_0:0
pkt_2_8_8_0:0
pkt_3_9_9_0:2
state_group_0_state_0_a_a_0:0
state_group_1_state_0_b_b_0:0
BEG FIND
Level 1 intsize = 2
* After optims it became = 17598 was 17618
* After all optims it became = 17598
finder hits = 1409272 bstoreObjs=205202 sstorePages=399
hitcount 1 47319 5
hitcount 2 30153 5
hitcount 3 14060 5
hitcount 4 55821 5
hitcount 5 8879 5
hitcount 6 1024 5
hitcount 7 767 5
hitcount 8 4 5
hitcount 9 4082 5
hitcount 10 380 5
hitcount 11 2265 5
hitcount 12 8 5
hitcount 13 132 5
hitcount 14 48 6
hitcount 15 4 5
hitcount 16 1224 5
hitcount 19 13646 5
hitcount 20 4 6
hitcount 21 8 6
hitcount 23 1424 5
hitcount 24 21896 5
hitcount 25 4 5
hitcount 27 4 6
hitcount 28 8 6
hitcount 29 1230 5
hitcount 31 12 4
hitcount 33 4 5
hitcount 34 172 5
hitcount 39 116 5
hitcount 41 22 5
hitcount 42 16 5
hitcount 44 8 4
hitcount 45 16 5
hitcount 47 46 5
hitcount 48 6 6
hitcount 49 198 5
hitcount 50 24 5
hitcount 52 8 6
hitcount 53 12 6
hitcount 55 4 6
hitcount 56 4 5
hitcount 57 4 6
hitcount 59 24 6
hitcount 74 80 5
hitcount 89 32 5
bucketsPerDepth 7 1023
bucketsPerDepth 8 1
* TIME TO ADD INPUT : 999.348 ms
DECISIONS START = 6687104
f# %assign: 0 clauses: 4370940 learn: 1133085 restart: 101 decision: 6688003 propagated: 48498510922
END FIND
!+ 00111111000101100010010010000011100001110010001101000001010111011111010011110010000101100010101111000100111010111100011111010011011000000011000001101000001001000011111111010101010000001100000100001111010001000001000100010001101101011001001011100100100100010101000100011000001000110010100110000100100100010100001000110001010110100110100010010010111001110000100101010001000101111011010101001101010101011111101001110100101000100000000011111011000011011010010000010011110001
!+ H__0:0
H__1:3
H__3:15
H__5:0
H__6:1
H__8:3
H__10:1
H__11:2
H__13:4
H__15:0
H__16:2
H__18:3
H__34:2
H__35:3
H__37:4
H__39:2
H__40:1
H__42:1
H__44:2
H__45:2
H__47:14
H__49:3
H__50:3
H__52:5
H__68:3
H__69:3
H__71:4
H__73:0
H__74:1
H__76:3
H__78:1
H__79:1
H__81:15
H__83:0
H__84:1
H__86:14
H__102:1
H__103:3
H__105:3
H__107:3
H__108:3
H__110:5
H__112:3
H__113:2
H__115:1
H__117:0
H__118:2
H__120:1
H__136:2
H__137:1
H__139:1
H__141:2
H__142:0
H__144:1
H__146:3
H__147:3
H__149:15
H__151:1
H__152:1
H__154:5
H__218:0
H__216:0
H__214:0
H__212:0
H__210:1
H__219:1
H__217:0
H__215:0
H__213:0
H__211:0
H__26:2
H__33:0
H__60:0
H__67:3
H__94:3
H__101:2
H__128:0
H__135:2
H__162:0
H__169:0
H__20:2
H__171:0
H__24:2
H__170:0
H__22:0
H__21:1
H__25:0
H__23:1
H__54:1
H__175:3
H__191:2
H__9:2
H__7:1
H__192:2
H__14:0
H__12:1
H__193:3
H__19:1
H__17:2
H__190:0
H__4:1
H__2:2
H__58:0
H__174:2
H__56:0
H__55:1
H__59:1
H__57:0
H__88:2
H__179:0
H__195:2
H__27:1
H__173:0
H__31:0
H__172:1
H__29:0
H__28:2
H__32:1
H__30:0
H__43:1
H__41:1
H__196:2
H__48:1
H__46:0
H__197:2
H__53:0
H__51:1
H__194:2
H__38:0
H__36:2
H__92:2
H__178:0
H__90:0
H__89:2
H__93:0
H__91:0
H__122:3
H__183:0
H__199:2
H__61:2
H__177:2
H__65:1
H__176:1
H__63:0
H__62:3
H__66:2
H__64:0
H__77:0
H__75:1
H__200:2
H__82:0
H__80:1
H__201:3
H__87:1
H__85:2
H__198:3
H__72:0
H__70:0
H__126:1
H__182:2
H__124:0
H__123:1
H__127:1
H__125:0
H__156:2
H__187:0
H__203:2
H__95:2
H__181:3
H__99:1
H__180:3
H__97:0
H__96:1
H__100:1
H__98:1
H__111:0
H__109:3
H__204:2
H__116:2
H__114:2
H__205:2
H__121:2
H__119:3
H__202:3
H__106:1
H__104:1
H__160:2
H__186:3
H__158:0
H__157:1
H__161:2
H__159:0
H__129:1
H__185:0
H__133:1
H__184:0
H__131:0
H__130:0
H__134:0
H__132:0
H__163:3
H__189:3
H__167:1
H__188:3
H__165:0
H__164:0
H__168:2
H__166:1
H__206:2
H__140:1
H__138:1
H__207:2
H__145:0
H__143:0
H__208:2
H__150:0
H__148:3
H__209:3
H__155:0
H__153:2
BEG CHECK
* After optims it became = 48 was 17618
Assert at flowlet..tion_2.sk:4066 (1)
Simulation found a cex by random testing: 0 ms
END CHECK
******** 6 ftime= 9999.88 ctime= 0.029
!% 001001000110
!% pkt_0_6_6_0:0
pkt_1_7_7_0:1
pkt_2_8_8_0:2
pkt_3_9_9_0:0
state_group_0_state_0_a_a_0:2
state_group_1_state_0_b_b_0:1
BEG FIND
Level 1 intsize = 2
* After optims it became = 17589 was 17618
* After all optims it became = 17589
finder hits = 1709661 bstoreObjs=248274 sstorePages=499
hitcount 0 42275 7
hitcount 1 13545 5
hitcount 2 42013 5
hitcount 3 36572 5
hitcount 4 21211 5
hitcount 5 34990 5
hitcount 6 9567 5
hitcount 7 898 5
hitcount 8 16 6
hitcount 9 218 5
hitcount 10 116 5
hitcount 11 4148 5
hitcount 13 1746 5
hitcount 14 60 5
hitcount 15 635 5
hitcount 17 8 6
hitcount 18 1224 5
hitcount 19 293 5
hitcount 22 16 5
hitcount 23 13349 5
hitcount 27 1424 5
hitcount 29 21900 5
hitcount 31 16 4
hitcount 34 1234 5
hitcount 35 4 6
hitcount 37 4 5
hitcount 39 4 6
hitcount 41 172 5
hitcount 47 112 5
hitcount 48 22 5
hitcount 49 16 5
hitcount 52 8 4
hitcount 53 16 5
hitcount 55 46 5
hitcount 56 29 5
hitcount 57 21 6
hitcount 59 178 5
hitcount 61 8 6
hitcount 62 12 6
hitcount 63 4 6
hitcount 64 4 5
hitcount 69 28 6
hitcount 89 80 5
hitcount 104 32 5
bucketsPerDepth 8 5
bucketsPerDepth 9 602
bucketsPerDepth 10 375
bucketsPerDepth 11 40
bucketsPerDepth 12 2
* TIME TO ADD INPUT : 999.366 ms
DECISIONS START = 6688003
----- Statistics -----
Total elapsed time (ms): 4.4499e+07
Model building time (ms): 0.044
Solution time (ms): 0
Max virtual mem (bytes): 3881164800
Max resident mem (bytes): 3740319744
Max private mem (bytes): 3876368384
cegis: core/Solver.cpp:577: void MSsolverNS::Solver::analyze(MSsolverNS::Clause*, MSsolverNS::vec<MSsolverNS::Lit>&, int&): Assertion `confl != NULL' failed.
Someone threw a C-style assertion.
[SATBackend] Stats for last run:
[solution stats]
successful? ---------------------> false
elapsed time (s) ----------------> 44499.336
model building time (s) ---------> -0.001
solution time (s) ---------------> -0.001
max memory usage (MiB) ----------> -9.536743E-7
[SAT-specific solution stats]
initial number of nodes ---------> -1
number of nodes after opts ------> -1
number of controls --------------> -1
total number of control bits ----> -1
[SATBackend] Solver exit value: 3
[SATBackend] The sketch cannot be resolved.
[1557993462.0170 - ERROR] [SKETCH] Sketch Not Resolved Error: cegis: core/Solver.cpp:577: void MSsolverNS::Solver::analyze(MSsolverNS::Clause*, MSsolverNS::vec<MSsolverNS::Lit>&, int&): Assertion `confl != NULL' failed.
Someone threw a C-style assertion.
The sketch could not be resolved.
[1557993462.0180 - DEBUG] [SKETCH] stack trace written to file: /home/taegyunk/.sketch/tmp/stacktrace.txt
[1557993462.0190 - DEBUG] Backend solver input file at /home/taegyunk/.sketch/tmp/flowlets_pred_raw_stateless_alu_5_4_codegen_iteration_2.sk/input0.tmp
Total time = 44500373
Command exited with non-zero status 1
44286.29user 241.68system 12:21:40elapsed 100%CPU (0avgtext+0avgdata 3652724maxresident)k
0inputs+24608outputs (0major+309595754minor)pagefaults 0swaps
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment