aterga

docker build -t IMAGE_NAME
docker run -it -d --name INSTANCE_NAME IMAGE_NAME
docker exec -it INSTANCE_NAME /bin/bash

aterga

#!/bin/bash

printf "$1,"
RESPONSE=$((
        (echo "(set-option :produce-unsat-cores true)"); 
        (echo "(set-option :smt.core.minimize true)");
        (cat $1); 
        (echo "(get-unsat-core)") 
) | z3 -smt2 -in)
if echo $RESPONSE | grep -q unknown; 

aterga

for dir in *; 
do 
  for file in $dir/*; 
  do 
    $(vampire 
      --mode casc 
      --input_syntax smtlib2 
      --time_limit 18000s 
      --memory_limit 2000000 
      --random_seed 0 

aterga

N_FILES_IN_GROUP=333
TIMEOUT_PER_RUN_SEC=2000
i=0; for f in *.smt2; do d=group_$(printf %03d $((i/$N_FILES_IN_GROUP+1))); mkdir -p $d; mv "$f" $d; let i++; done
for dir in *; do python ~/axiom-testing-project/axioms/src/minimizer/main.py --is_debug=false --timeout $TIMEOUT_PER_RUN_SEC --location $dir mine_dummies & echo $! >> active_pids.txt; done; wait; echo ">>> Processed all groups. <<<"; rm -f active_pids.txt
# You can use "kill -9 $(cat active_pids.txt)" to terminate all Python sub-processes started by the command above. 

aterga

for file in *.vpr; do java -Xmx2048m -Xss16m -cp :/usr/local/Viper/backends/*.jar viper.carbon.Carbon --z3Exe "/usr/local/Viper/z3/bin/z3" --boogieExe "/usr/local/Viper/boogie/Binaries/Boogie.exe" --proverLog "$file.smt2" $file ; done

aterga

#!/bin/bash

####################################################################################
## Move files that match pattern while preserving origin directory information. 
## Run as follows: 
##
##  find non-incremental/ -type f -name "*.smt2" -exec ./move.sh "forall" {} \;
##
####################################################################################

aterga

field f: Ref 

define CLOSED(nodes)
    (forall n:Ref :: { n in nodes, n.f } n in nodes && n.f != null ==> n.f in nodes)

define STRUCT(nodes)
    (forall n:Ref :: { n.f } n in nodes ==> acc(n.f)) && 
    !(null in nodes) && 
    CLOSED(nodes)

aterga

field next: Ref
field value: Int

predicate lseg(this: Ref, end: Ref) {
    acc(this.value, write) && acc(this.next, write) &&
       (this.next != end ==> this.next != null && acc(lseg(this.next, end), write))
}

function get(this: Ref, i: Int, end: Ref): Int
    requires acc(lseg(this, end), write)

aterga

const N: int;
axiom 1 < N;
var a: [int]int;
var perm: [int]int;

procedure __new_perm__() returns (perm: [int]int)
	ensures perm_ok(perm);
	ensures (forall k: int :: 0 <= k && k < N ==> perm[k] == k);
{
 	var n: int; n := 0;

aterga

// class Node
field left: Ref
field right: Ref
field is_marked: Bool

predicate inv(node: Ref, graph: Set[Ref]) {
	   node != null
	&& acc(node.left)
	&& acc(node.right)
	&& acc(node.is_marked)