# Boolector: Satisfiablity Modulo Theories (SMT) solver. # # Copyright (C) 2007-2021 by the authors listed in the AUTHORS file. # # This file is part of Boolector. # See COPYING for more information on using this software. # find_package(GoogleTest REQUIRED) set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin/tests) set(test_names aig aigvec arithmetic boolectornodemap bv comp exp hash inc inthash inthashmap lambda logic mc mem misc modelgen modelgensmt2 nodemap normquant overflow parseerror prop propinv rotate queue satmgr shift smtaxioms sort stack unionfind util ) foreach(test ${test_names}) add_executable (test${test} test_${test}.cpp) target_include_directories(test${test} PRIVATE ${PROJECT_SOURCE_DIR}/test/new_test) target_link_libraries(test${test} boolector m) target_link_libraries(test${test} GTest::gtest_main) set_target_properties(test${test} PROPERTIES OUTPUT_NAME test${test}) add_test(${test} ${CMAKE_BINARY_DIR}/bin/tests/test${test}) endforeach() set(sat_testcases "arraycond1.btor" "arraycond10.btor" "arraycond15.btor" "arraycond16.btor" "arraycond17.btor" "arraycond2.btor" "arraycond4.btor" "const1.btor" "constarray.smt2" "ext1.btor" "ext12.btor" "ext14.btor" "ext17.btor" "ext20.btor" "ext3.btor" "ext4.btor" "ext6.btor" "ext8.btor" "extarraywrite3sat.smt2" "factor18446744073709551617const.btor" "factor18446744073709551617xconst.btor" "factor18446744073709551617yconst.btor" "factor2209.btor" "factor4294967295.btor" "factor4294967297.btor" "fifo32ia04k05.smt2" "fifo32in04k05.smt2" "invalidmodel1.smt2" "invalidmodel2.smt2 -xl=0 -ml=0 -rwl=2" "invalidmodel3.btor" "issue96.smt2" "lazyreadwritebug1.btor" "lambda1.btor" "lin0.btor" "lin1.btor" "lin2.btor" "lin3.btor" "lin4.btor" "nestedfun1.smt2 -rwl 2" "normaddneg0.btor" "normaddneg1.btor" "proxybug.btor" "random1.btor" "random1.btor2" "random2.btor" "random3.btor" "random4.btor" "read12.btor" "read13.btor" "read14.btor" "read15.btor" "read18.btor" "read3.btor" "redand3twice.btor" "redor3.btor" "regr3vl1.btor -rwl 0" "regr3vl1.btor -rwl 1" "regr3vl1.btor -rwl 2" "regr3vl1.btor -rwl 3" "regr3vl2.btor -rwl 0" "regr3vl2.btor -rwl 1" "regr3vl2.btor -rwl 2" "regr3vl2.btor -rwl 3" "regr3vl3.btor -rwl 0" "regr3vl3.btor -rwl 1" "regr3vl3.btor -rwl 2" "regr3vl3.btor -rwl 3" "regr3vl4.btor -rwl 0" "regr3vl4.btor -rwl 1" "regr3vl4.btor -rwl 2" "regr3vl4.btor -rwl 3" "regrbetacache1.btor -br all" # currently broken since we don't allow to mix lambdas with arrays #"regrbetacache2.btor -br all" "regrbfs1.btor -rwl 0" "regrbfs1.btor -rwl 1" "regrbfs1.btor -rwl 2" "regrbfs1.btor -rwl 3" "regrcollectprem.btor" "regrdomabst1.btor" "regrdomabst2.btor" "regrdomabst3.btor" "regrdomabst4.btor" "regrembeddedconstraint10.btor -rwl 0" "regrembeddedconstraint10.btor -rwl 1" "regrembeddedconstraint10.btor -rwl 2" "regrembeddedconstraint10.btor -rwl 3" "regrembeddedconstraint11.btor -rwl 0" "regrembeddedconstraint11.btor -rwl 1" "regrembeddedconstraint11.btor -rwl 2" "regrembeddedconstraint11.btor -rwl 3" "regrembeddedconstraint3.btor -rwl 0" "regrembeddedconstraint3.btor -rwl 1" "regrembeddedconstraint3.btor -rwl 2" "regrembeddedconstraint3.btor -rwl 3" "regrembeddedconstraint5.btor -rwl 0" "regrembeddedconstraint5.btor -rwl 1" "regrembeddedconstraint5.btor -rwl 2" "regrembeddedconstraint5.btor -rwl 3" "regrembeddedconstraint6.btor -rwl 0" "regrembeddedconstraint6.btor -rwl 1" "regrembeddedconstraint6.btor -rwl 2" "regrembeddedconstraint6.btor -rwl 3" "regrembeddedconstraint7.btor -rwl 0" "regrembeddedconstraint7.btor -rwl 1" "regrembeddedconstraint7.btor -rwl 2" "regrembeddedconstraint7.btor -rwl 3" "regrembeddedconstraint8.btor -rwl 0" "regrembeddedconstraint8.btor -rwl 1" "regrembeddedconstraint8.btor -rwl 2" "regrembeddedconstraint8.btor -rwl 3" "regrembeddedconstraint9.btor -rwl 0" "regrembeddedconstraint9.btor -rwl 1" "regrembeddedconstraint9.btor -rwl 2" "regrembeddedconstraint9.btor -rwl 3" "regrencparamapps.smt2" "regrlemmaloop_embeddedconstraints.btor -rwl 1" "regrmark1.btor -rwl 0" "regrmark1.btor -rwl 1" "regrmark1.btor -rwl 2" "regrmark1.btor -rwl 3" "regrmodel1.btor" "regrmodel3.btor" "regrmodel4.btor" "regpicoprepsqrt4.btor" "regprim11simp.btor" "regrrwbinexpconcatzeroconst.btor" "regrw8simp.btor" "rol_same_bw.btor" "ror_same_bw.btor" "rw113.btor -rwl 0" "rw1.btor" "rw10.btor" "rw11.btor" "rw12.btor" "rw13.btor" "rw14.btor" "rw15.btor" "rw2.btor" "rw3.btor" "rw4.btor" "rw5.btor" "rw6.btor" "rw7.btor" "rw8.btor" "rw9.btor" "rw113.btor -rwl 1" "rw114.btor -rwl 0" "rw114.btor -rwl 1" "rw121.btor -rwl 0" "rw121.btor -rwl 1" "rw122.btor -rwl 0" "rw122.btor -rwl 1" "rw132.btor -rwl 0" "rw132.btor -rwl 1" "rw133.btor -rwl 0" "rw133.btor -rwl 1" "rw134.btor -rwl 0" "rw134.btor -rwl 3" "rw135.btor -rwl 0" "rw135.btor -rwl 3" "rw137.btor -rwl 0" "rw137.btor -rwl 3" "rw138.btor -rwl 0" "rw138.btor -rwl 3" "rw139.btor -rwl 0" "rw139.btor -rwl 3" "rw140.btor -rwl 0" "rw140.btor -rwl 3" "rw141.btor -rwl 0" "rw141.btor -rwl 3" "rw142.btor -rwl 0" "rw142.btor -rwl 3" "rw143.btor -rwl 0" "rw143.btor -rwl 3" "rw148.btor -rwl 0" "rw148.btor -rwl 3" "rw153.btor -rwl 0" "rw153.btor -rwl 3" "rw157.btor" "rw16.btor -rwl 0" "rw16.btor -rwl 1" "rw166.btor -rwl 1" "rw167.btor -rwl 1" "rw168.btor -rwl 1" "rw169.btor -rwl 1" "rw17.btor -rwl 0" "rw17.btor -rwl 1" "rw178.btor -rwl 3" "rw179.btor -rwl 3" "rw18.btor -rwl 0" "rw18.btor -rwl 1" "rw212.smt2 -rwl 3" "rw216.smt2 -rwl 3" "rw44.btor -rwl 0" "rw44.btor -rwl 1" "rw45.btor -rwl 0" "rw45.btor -rwl 1" "rw58.btor -rwl 0" "rw58.btor -rwl 3" "rw59.btor -rwl 0" "rw59.btor -rwl 3" "rwpropindexpluszero1.btor" "rwpropindexpluszero1.btor -rwl 0" "rwpropindexpluszero2.btor" "rwpropindexpluszero2.btor -rwl 0" "rwpropindexpluszero3.btor" "rwpropindexpluszero3.btor -rwl 0" "rwpropindexpluszero4.btor" "rwpropindexpluszero4.btor -rwl 0" "rwpropindexpluszero5.btor" "rwpropindexpluszero5.btor -rwl 0" "rwpropindexpluszero6.btor" "rwpropindexpluszero6.btor -rwl 0" "rwpropindexpluszero7.btor" "rwpropindexpluszero7.btor -rwl 0" "rwpropindexpluszero8.btor" "rwpropindexpluszero8.btor -rwl 0" "rwr1.btor -rwl 3 -br all" "rww1.btor -rwl 3" "sc12fuzzcheck2.smt2" "slicesubst1.btor -rwl 0" "slicesubst1.btor -rwl 2" "sll_same_bw.btor" "smt2pushpop0.smt2 -i" "smtashr1.smt2" "smtashr2.smt2" "smtashr3.smt2" "smtextarray1sat0.smt2" "smtextarray1sat1.smt2" "smtextarray2sat0.smt2" "smtextarray2sat1.smt2" "smtextarray2sat2.smt2" "smtextarray2sat3.smt2" "smtextarray3sat0.smt2" "smtextarray3sat1.smt2" "smtextarray3sat2.smt2" "smtextarray3sat3.smt2" "smtextarray3sat4.smt2" "smtextarray3sat5.smt2" "smtextarray3sat6.smt2" "smtextarray3sat7.smt2" "smtlshr1.smt2" "smtlshr2.smt2" "smtlshr3.smt2" "smtrepeat.smt2" "smtrotate.smt2" "smtshl1.smt2" "smtshl2.smt2" "smtshl3.smt2" "smtsignextend.smt2" "smttrue.smt2" "smtzeroextend.smt2" "sqrt25.btor" "sqrt4.btor" "sqrt4295098369.btor" "sqrt49.btor" "sqrt9.btor" "srl_same_bw.btor" "substcyclic1.btor" "substitute1.btor" "substitute3.btor" "substitute4.btor" "substitute40.btor" "substitute5.btor" "swapmem002se.smt2" "ultsubst1.btor -rwl 0" "ultsubst1.btor -rwl 2" "ultsubst2.btor -rwl 0" "ultsubst2.btor -rwl 2" "ultsubst3.btor -rwl 0" "ultsubst3.btor -rwl 2" "ultsubst4.btor -rwl 0" "ultsubst4.btor -rwl 2" "ultsubst5.btor -rwl 0" "ultsubst5.btor -rwl 2" "ultsubst6.btor -rwl 0" "ultsubst6.btor -rwl 2" "ultsubst7.btor -rwl 0" "ultsubst7.btor -rwl 2" "ultsubst8.btor -rwl 0" "ultsubst8.btor -rwl 2" "ultsubst9.btor -rwl 0" "ultsubst9.btor -rwl 2" "upprop1.btor" "var1.btor" "var2.btor" "write11.btor" "write12.btor" "write15.btor" "write18.btor" "write19.btor" "write20.btor" "write5.btor" "wchains002se.smt2" ) set(unsat_testcases "3vl1.btor -rwl 0" "3vl1.btor -rwl 2" "3vl2.btor -rwl 0" "3vl2.btor -rwl 2" "3vl3.btor -rwl 0" "3vl3.btor -rwl 2" "3vl4.btor -rwl 0" "3vl4.btor -rwl 2" "3vl5.btor -rwl 0" "3vl5.btor -rwl 2" "3vl6.btor -rwl 0" "3vl6.btor -rwl 2" "addnegmul1.btor" "andopt1.btor" "andopt10.btor" "andopt11.btor" "andopt12.btor" "andopt13.btor" "andopt14.btor" "andopt15.btor" "andopt16.btor" "andopt17.btor" "andopt2.btor" "andopt3.btor" "andopt4.btor" "andopt5.btor" "andopt6.btor" "andopt7.btor" "andopt8.btor" "andopt9.btor" "arraycond11.btor" "arraycond12.btor" "arraycond13.btor" "arraycond14.btor" "arraycond18.btor" "arraycond3.btor" "arraycond5.btor" "arraycond6.btor" "arraycond7.btor" "arraycond8.btor" "arraycond9.btor" "arraycondconst.btor -rwl 0" "arraycondconstaig.btor -rwl 0" "binarysearch32s016.smt2" "bubsort002un.smt2" "const2.btor" "countbits016.smt2" "dec_rwl3.btor" "dec_rwl0.btor -rwl 0" "distri1.btor" "distri2.btor" "distri3.btor" "distri4.btor" "distri5.btor" "distri6.btor" "distri7.btor" "distri8.btor" "dubreva002ue.smt2" "exactlyone.btor" "ext10.btor" "ext11.btor" "ext13.btor" "ext15.btor" "ext16.btor" "ext18.btor" "ext19.btor" "ext2.btor" "ext21.btor" "ext22.btor" "ext23.btor" "ext24.btor" "ext25.btor" "ext26.btor" "ext27.btor" "ext28.btor" "ext29.btor" "ext5.btor" "ext7.btor" "ext9.btor" "extarraywrite1.btor" "extarraywrite2.btor" "extarraywrite3.smt2" "fifo32bc04k05.smt2" "gtewithsub.btor" "hd1.btor -rwl 0" "hd1.btor -rwl 1" "hd10.btor -rwl 0" "hd10.btor -rwl 1" "hd11.btor -rwl 0" "hd11.btor -rwl 1" "hd12.btor -rwl 0" "hd12.btor -rwl 1" "hd13.btor -rwl 0" "hd13.btor -rwl 1" "hd14.btor -rwl 0" "hd14.btor -rwl 1" "hd15.btor -rwl 0" "hd15.btor -rwl 1" "hd16.btor -rwl 0" "hd16.btor -rwl 1" "hd17.btor -rwl 0" "hd17.btor -rwl 1" "hd18.btor -rwl 0" "hd18.btor -rwl 1" "hd19.btor" "hd2.btor -rwl 0" "hd2.btor -rwl 1" "hd20.btor" "hd21.btor" "hd3.btor -rwl 0" "hd3.btor -rwl 1" "hd4.btor -rwl 0" "hd4.btor -rwl 1" "hd5.btor -rwl 0" "hd5.btor -rwl 1" "hd6.btor -rwl 0" "hd6.btor -rwl 1" "hd7.btor -rwl 0" "hd7.btor -rwl 1" "hd8.btor -rwl 0" "hd8.btor -rwl 1" "hd9.btor -rwl 0" "hd9.btor -rwl 1" "inc.btor" "inc.btor -rwl 0" "issue97.smt2" "lambda2.btor" "memcpy02.smt2" "mulassoc4.smt2" "mulassoc5.smt2" "mulassoc6.smt2" "nextpoweroftwo016.smt2" "normaddneg2.btor" "normaddneg3.btor" "prim8bugreduced.btor" "problem_130.smt2" "random5.btor -rwl 0" "random5.btor -rwl 1" "read1.btor" "read10.btor" "read11.btor" "read16.btor" "read17.btor" "read19.btor" "read2.btor" "read20.btor" "read21.btor" "read22.btor" "read4.btor" "read5.btor" "read6.btor" "read7.btor" "read8.btor" "read9.btor" "regr-distinct.smt2" "regrcalypto1.smt2" "regrcalypto2.smt2" "regrcalypto3.smt2" "regrembeddedconstraint1.btor -rwl 0" "regrembeddedconstraint1.btor -rwl 1" "regrembeddedconstraint1.btor -rwl 2" "regrembeddedconstraint1.btor -rwl 3" "regrembeddedconstraint12.btor -rwl 0" "regrembeddedconstraint12.btor -rwl 1" "regrembeddedconstraint12.btor -rwl 2" "regrembeddedconstraint12.btor -rwl 3" "regrembeddedconstraint13.btor -rwl 0" "regrembeddedconstraint13.btor -rwl 1" "regrembeddedconstraint13.btor -rwl 2" "regrembeddedconstraint13.btor -rwl 3" "regrembeddedconstraint14.btor -rwl 0" "regrembeddedconstraint14.btor -rwl 1" "regrembeddedconstraint14.btor -rwl 2" "regrembeddedconstraint14.btor -rwl 3" "regrembeddedconstraint2.btor -rwl 0" "regrembeddedconstraint2.btor -rwl 1" "regrembeddedconstraint2.btor -rwl 2" "regrembeddedconstraint2.btor -rwl 3" "regrembeddedconstraint4.btor -rwl 0" "regrembeddedconstraint4.btor -rwl 1" "regrembeddedconstraint4.btor -rwl 2" "regrembeddedconstraint4.btor -rwl 3" "regrexpleak1.btor -rwl 0" "regrexpleak1.btor -rwl 1" "regrexpleak1.btor -rwl 2" "regrexpleak1.btor -rwl 3" "regrexpleak2.btor -rwl 0" "regrexpleak2.btor -rwl 1" "regrexpleak2.btor -rwl 2" "regrexpleak2.btor -rwl 3" "regrnormquant.smt2" "regrmark2.btor -rwl 0" "regrmark2.btor -rwl 1" "regrmark2.btor -rwl 2" "regrmark2.btor -rwl 3" "regrmark3.btor -rwl 0" "regrmark3.btor -rwl 1" "regrmark3.btor -rwl 2" "regrmark3.btor -rwl 3" "regrmodel2.btor" "regrpointerchasing1.btor" "regsmod1.smt2" "regsmtparselet.smt2" "regsubslapd149921red.btor" "rw100.btor -rwl 0" "rw100.btor -rwl 1" "rw101.btor -rwl 0" "rw101.btor -rwl 1" "rw102.btor -rwl 0" "rw102.btor -rwl 1" "rw103.btor -rwl 0" "rw103.btor -rwl 1" "rw104.btor -rwl 0" "rw104.btor -rwl 1" "rw105.btor -rwl 0" "rw105.btor -rwl 1" "rw106.btor -rwl 0" "rw106.btor -rwl 1" "rw107.btor -rwl 0" "rw107.btor -rwl 1" "rw108.btor -rwl 0" "rw108.btor -rwl 1" "rw109.btor -rwl 0" "rw109.btor -rwl 1" "rw110.btor -rwl 0" "rw110.btor -rwl 1" "rw111.btor -rwl 0" "rw111.btor -rwl 1" "rw112.btor -rwl 0" "rw112.btor -rwl 1" "rw115.btor -rwl 0" "rw115.btor -rwl 1" "rw116.btor -rwl 0" "rw116.btor -rwl 1" "rw117.btor -rwl 0" "rw117.btor -rwl 1" "rw118.btor -rwl 0" "rw118.btor -rwl 1" "rw119.btor -rwl 0" "rw119.btor -rwl 1" "rw120.btor -rwl 0" "rw120.btor -rwl 1" "rw123.btor -rwl 0" "rw123.btor -rwl 1" "rw124.btor -rwl 0" "rw124.btor -rwl 1" "rw125.btor -rwl 0" "rw125.btor -rwl 3" "rw126.btor -rwl 0" "rw126.btor -rwl 3" "rw127.btor -rwl 0" "rw127.btor -rwl 3" "rw128.btor -rwl 0" "rw128.btor -rwl 3" "rw129.btor -rwl 0" "rw129.btor -rwl 3" "rw130.btor -rwl 0" "rw130.btor -rwl 1" "rw131.btor -rwl 0" "rw131.btor -rwl 1" "rw136.btor -rwl 0" "rw136.btor -rwl 3" "rw144.btor -rwl 0" "rw144.btor -rwl 3" "rw145.btor -rwl 0" "rw145.btor -rwl 3" "rw146.btor -rwl 0" "rw146.btor -rwl 3" "rw147.btor -rwl 0" "rw147.btor -rwl 3" "rw149.btor -rwl 0" "rw149.btor -rwl 3" "rw150.btor -rwl 0" "rw150.btor -rwl 3" "rw151.btor -rwl 0" "rw151.btor -rwl 3" "rw152.btor -rwl 0" "rw152.btor -rwl 3" "rw154.btor -rwl 0" "rw154.btor -rwl 1" "rw155.btor -rwl 0" "rw155.btor -rwl 1" "rw156.btor -rwl 0" "rw156.btor -rwl 1" "rw158.btor -rwl 1" "rw159.btor -rwl 1" "rw160.btor -rwl 1" "rw161.btor -rwl 1" "rw162.btor -rwl 1" "rw163.btor -rwl 1" "rw164.btor -rwl 1" "rw165.btor -rwl 1" "rw170.btor -rwl 1" "rw171.btor -rwl 1" "rw172.btor -rwl 1" "rw173.btor -rwl 1" "rw174.btor -rwl 1" "rw175.btor -rwl 1" "rw176.btor -rwl 1" "rw177.btor -rwl 1" "rw180.btor -rwl 3" "rw181.btor -rwl 3" "rw182.btor -rwl 3" "rw183.btor -rwl 3" "rw184.btor -rwl 3" "rw185.btor -rwl 3" "rw186.btor -rwl 3" "rw187.btor -rwl 3" "rw188.btor -rwl 3" "rw189.btor -rwl 3" "rw19.btor -rwl 0" "rw19.btor -rwl 1" "rw190.btor -rwl 3" "rw191.btor -rwl 3" "rw192.btor -rwl 3" "rw193.btor -rwl 3" "rw194.btor -rwl 3" "rw195.btor -rwl 3" "rw196.btor -rwl 3" "rw197.btor -rwl 3" "rw198.btor -rwl 3" "rw199.btor -rwl 3" "rw20.btor -rwl 0" "rw20.btor -rwl 1" "rw200.btor -rwl 3" "rw201.btor -rwl 3" "rw202.btor -rwl 3" "rw203.btor -rwl 3" "rw204.btor -rwl 3" "rw205.btor -rwl 3" "rw206.btor -rwl 3" "rw207.btor -rwl 3" "rw208.btor -rwl 3" "rw209.btor -rwl 3" "rw21.btor -rwl 0" "rw21.btor -rwl 1" "rw210.btor -rwl 3" "rw211.btor -rwl 3" "rw213.smt2 -rwl 3" "rw214.smt2 -rwl 3" "rw215.smt2 -rwl 3" "rw217.smt2 -rwl 3" "rw218.smt2 -rwl 3" "rw219.smt2 -rwl 3" "rw22.btor -rwl 0" "rw22.btor -rwl 1" "rw220.smt2 -rwl 3" "rw221.smt2 -rwl 3" "rw23.btor -rwl 0" "rw23.btor -rwl 1" "rw24.btor -rwl 0" "rw24.btor -rwl 1" "rw25.btor -rwl 0" "rw25.btor -rwl 1" "rw26.btor -rwl 0" "rw26.btor -rwl 1" "rw27.btor -rwl 0" "rw27.btor -rwl 1" "rw28.btor -rwl 0" "rw28.btor -rwl 1" "rw29.btor -rwl 0" "rw29.btor -rwl 1" "rw30.btor -rwl 0" "rw30.btor -rwl 1" "rw31.btor -rwl 0" "rw31.btor -rwl 1" "rw32.btor -rwl 0" "rw32.btor -rwl 1" "rw33.btor -rwl 0" "rw33.btor -rwl 1" "rw34.btor -rwl 0" "rw34.btor -rwl 1" "rw35.btor -rwl 0" "rw35.btor -rwl 1" "rw36.btor -rwl 0" "rw36.btor -rwl 1" "rw37.btor -rwl 0" "rw37.btor -rwl 1" "rw38.btor -rwl 0" "rw38.btor -rwl 1" "rw39.btor -rwl 0" "rw39.btor -rwl 1" "rw40.btor -rwl 0" "rw40.btor -rwl 1" "rw41.btor -rwl 0" "rw41.btor -rwl 1" "rw42.btor -rwl 0" "rw42.btor -rwl 1" "rw43.btor -rwl 0" "rw43.btor -rwl 1" "rw46.btor" "rw47.btor" "rw48.btor" "rw49.btor" "rw50.btor" "rw51.btor" "rw52.btor -rwl 0" "rw52.btor -rwl 1" "rw53.btor -rwl 0" "rw53.btor -rwl 3" "rw54.btor -rwl 0" "rw54.btor -rwl 3" "rw55.btor -rwl 0" "rw55.btor -rwl 3" "rw56.btor -rwl 0" "rw56.btor -rwl 3" "rw57.btor -rwl 0" "rw57.btor -rwl 3" "rw60.btor" "rw61.btor -rwl 0" "rw61.btor -rwl 1" "rw62.btor -rwl 0" "rw62.btor -rwl 1" "rw63.btor -rwl 0" "rw63.btor -rwl 1" "rw64.btor -rwl 0" "rw64.btor -rwl 1" "rw65.btor -rwl 0" "rw65.btor -rwl 1" "rw66.btor -rwl 0" "rw66.btor -rwl 1" "rw67.btor -rwl 0" "rw67.btor -rwl 1" "rw68.btor -rwl 0" "rw68.btor -rwl 1" "rw69.btor -rwl 0" "rw69.btor -rwl 3" "rw70.btor -rwl 0" "rw70.btor -rwl 3" "rw71.btor -rwl 0" "rw71.btor -rwl 3" "rw72.btor -rwl 0" "rw72.btor -rwl 3" "rw73.btor -rwl 0" "rw73.btor -rwl 3" "rw74.btor -rwl 0" "rw74.btor -rwl 3" "rw75.btor -rwl 0" "rw75.btor -rwl 3" "rw76.btor -rwl 0" "rw76.btor -rwl 3" "rw77.btor -rwl 0" "rw77.btor -rwl 3" "rw78.btor -rwl 0" "rw78.btor -rwl 3" "rw79.btor -rwl 0" "rw79.btor -rwl 3" "rw80.btor -rwl 0" "rw80.btor -rwl 3" "rw81.btor -rwl 0" "rw81.btor -rwl 1" "rw82.btor -rwl 0" "rw82.btor -rwl 1" "rw83.btor -rwl 0" "rw83.btor -rwl 1" "rw84.btor -rwl 0" "rw84.btor -rwl 1" "rw85.btor -rwl 0" "rw85.btor -rwl 1" "rw86.btor -rwl 0" "rw86.btor -rwl 1" "rw87.btor -rwl 0" "rw87.btor -rwl 1" "rw88.btor -rwl 0" "rw88.btor -rwl 1" "rw89.btor -rwl 0" "rw89.btor -rwl 1" "rw90.btor -rwl 0" "rw90.btor -rwl 1" "rw91.btor -rwl 0" "rw91.btor -rwl 1" "rw92.btor -rwl 0" "rw92.btor -rwl 1" "rw93.btor -rwl 0" "rw93.btor -rwl 1" "rw94.btor -rwl 0" "rw94.btor -rwl 1" "rw95.btor -rwl 0" "rw95.btor -rwl 1" "rw96.btor -rwl 0" "rw96.btor -rwl 1" "rw97.btor -rwl 0" "rw97.btor -rwl 1" "rw98.btor -rwl 0" "rw98.btor -rwl 1" "rw99.btor -rwl 0" "rw99.btor -rwl 1" "rwpropindexplusconst1.btor" "rwpropindexplusconst1.btor -rwl 0" "rwpropindexplusconst2.btor" "rwpropindexplusconst2.btor -rwl 0" "rwpropindexplusconst3.btor" "rwpropindexplusconst3.btor -rwl 0" "rwpropindexplusconst4.btor" "rwpropindexplusconst4.btor -rwl 0" "selsort002un.smt2" "smtarraycond1.smt2" "smtarraycond2.smt2" "smtarraycond3.smt2" "smtaxiommccarthy.smt2" "smtbv255.smt2" "smtextarrayaxiom1.smt2" "smtextarrayaxiom1uf.smt2" "smtextarrayaxiom2.smt2" "smtextarrayaxiom2uf.smt2" "smtextarrayaxiom3.smt2" "smtextarrayaxiom3uf.smt2" "smtextarrayaxiom4.smt2" "smtextarrayaxiom4uf.smt2" "smtfalse.smt2" "smtflet.smt2" "sqrt13.btor" "sqrt18446744073709551617.btor" "sqrt29.btor" "sqrt31.btor" "sqrt4294967297.btor" "sqrt5.btor" "sqrt53.btor" "sqrt65537.btor" "sqrt7.btor" "substitute10.btor" "substitute11.btor" "substitute12.btor" "substitute13.btor" "substitute14.btor" "substitute15.btor" "substitute16.btor" "substitute17.btor" "substitute18.btor" "substitute19.btor" "substitute2.btor" "substitute20.btor" "substitute21.btor" "substitute22.btor" "substitute23.btor" "substitute24.btor" "substitute25.btor" "substitute26.btor" "substitute27.btor" "substitute28.btor" "substitute29.btor" "substitute30.btor" "substitute31.btor" "substitute32.btor" "substitute33.btor" "substitute34.btor" "substitute35.btor" "substitute36.btor" "substitute37.btor" "substitute38.btor" "substitute39.btor" "substitute6.btor" "substitute7.btor" "substitute8.btor" "substitute9.btor" "sult.btor" "sult2.btor" "swapmem002ue.smt2" "twocomplementassub.btor" "udiv16castdown8.btor" "udiv8castdown4.btor" "udiv8castdown5.btor" "udiv8castdown6.btor" "udiv8castdown7.btor" "udivtheorem1.btor" "ulttheorem1.btor" "uremtheorem1.btor" "uremudivaxiom4.btor" "uremudivaxiom4no.btor" "wchains002ue.smt2" "write1.btor" "write10.btor" "write13.btor" "write14.btor" "write16.btor" "write17.btor" "write2.btor" "write21.btor" "write22.btor" "write23.btor" "write24.btor" "write3.btor" "write4.btor" "write6.btor" "write7.btor" "write8.btor" "write9.btor" ) set(cmp_testcases "arrayeqerr0.btor" "arrayeqerr1.btor" "arrayeqerr2.btor" "concatslice1.btor -rwl 1 -db" "concatslice2.btor -rwl 1 -db" "dumpbtor1.btor -rwl 0 -db" # currently broken due to dumper support for args/apply #"dumpbtor2.btor -rwl 0 -db" "dumpbtor3.btor -db" "dumpsmt1.btor -rwl 0 -ds" "dumpsmt2.btor -rwl 0 -ds" "echo.smt2" "getvalue1.smt2" "getvalue2.smt2" "getvalue3.smt2" "normalize_add_incomplete.btor -db" "normalize_and_incomplete.btor -db" "normalize_mul_incomplete.btor -db" "painc.smt2 -i" "regaddnorm1.btor -db" "regaddnorm2.btor -db" "regmismatch.smt2" "regnegadd1.btor -db" "regr-5smod3.btor -m -d" "regr-5srem3.btor -m -d" "regr-6smod3.btor -m -d" "regr-6srem3.btor -m -d" "regr5smod-3.btor -m -d" "regr5srem-3.btor -m -d" "regr6smod-3.btor -m -d" "regr6srem-3.btor -m -d" "smtandvar.smt2 -m" "smtiff.smt2 -m" "smtnotvar.smt2 -m" "smtor.smt2 -m" "smtvar.smt2 -m" "smtxor.smt2 -m" ) if(CaDiCaL_FOUND) list(APPEND cmp_testcases "nondestr_subst1.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst10.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst11.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst12.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst13.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst14.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst15.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst16.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst17.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst18.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst19.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst2.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst20.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst3.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst4.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst5.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst6.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst7.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst8.smt2 -i --nondestr-subst -SE cadical" "nondestr_subst9.smt2 -i --nondestr-subst -SE cadical" ) endif() get_target_property(BOOLECTOR_BINARY_PATH boolector-bin RUNTIME_OUTPUT_DIRECTORY) set(BOOLECTOR_BINARY "${BOOLECTOR_BINARY_PATH}/boolector") set(RUN_TEST_CASE_SCRIPT ${CMAKE_CURRENT_LIST_DIR}/run-test-case.py) macro(add_test_case option testcase) string(REPLACE " " "_" TESTNAME ${testcase}) string(REPLACE "-" "" TESTNAME ${TESTNAME}) set(tcase "${CMAKE_CURRENT_LIST_DIR}/log/${testcase}") add_test(${TESTNAME} ${RUN_TEST_CASE_SCRIPT} ${option} ${BOOLECTOR_BINARY} ${tcase} ${CMAKE_CURRENT_BINARY_DIR} ) set_tests_properties(${TESTNAME} PROPERTIES LABELS "testcases") endmacro() foreach(testcase ${sat_testcases}) add_test_case("--check-sat" ${testcase}) endforeach() foreach(testcase ${unsat_testcases}) add_test_case("--check-unsat" ${testcase}) endforeach() foreach(testcase ${cmp_testcases}) add_test_case("--check-output" ${testcase}) endforeach()