###
# Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
#
# This file is part of Bitwuzla.
#
# Copyright (C) 2007-2022 by the authors listed in the AUTHORS file.
#
# 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
  bv
  bvdomain
  bvdomaingen
  bvprop
  comp
  constbits
  essutils
  exp
  hash
  inc
  inthash
  inthashmap
  invutils
  lambda
  logic
  mem
  misc
  modelgen
  modelgensmt2
  nodemap
  normquant
  overflow
  prop
  propcomplete
  propcons
  propinv
  rotate
  queue
  satmgr
  shift
  smtaxioms
  sort
  stack
  unionfind
  util
)

if(SymFPU_FOUND)
  list(APPEND test_names api fp)
endif()

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} bitwuzla 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"
# Disabled since quantifiers disabled
#"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"
# Disabled since quantifiers disabled
#"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"
# Disabled since quantifiers disabled
#"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"

# parse error tests

"btorperr000.btor"
"btorperr001.btor"
"btorperr002.btor"
"btorperr003.btor"
"smt2perr000.smt2"
"smt2perr001.smt2"
"smt2perr002.smt2"
"smt2perr003.smt2"
"smt2perr004.smt2"
"smt2perr005.smt2"
"smt2perr006.smt2"
"smt2perr007.smt2"
"smt2perr008.smt2"
"smt2perr009.smt2"
"smt2perr011.smt2"
"smt2perr012.smt2"
"smt2perr013.smt2"
"smt2perr014.smt2"
"smt2perr015.smt2"
"smt2perr016.smt2"
"smt2perr017.smt2"
"smt2perr018.smt2"
"smt2perr019.smt2"
"smt2perr020.smt2"
"smt2perr021.smt2"
"smt2perr022.smt2"
"smt2perr023.smt2"
"smt2perr024.smt2"
"smt2perr025.smt2"
"smt2perr026.smt2"
"smt2perr027.smt2"
"smt2perr028.smt2"
"smt2perr029.smt2"
"smt2perr030.smt2"
"smt2perr031.smt2"
"smt2perr032.smt2"
"smt2perr033.smt2"
"smt2perr034.smt2"
"smt2perr035.smt2"
"smt2perr036.smt2"
"smt2perr037.smt2"
"smt2perr038.smt2"
"smt2perr039.smt2"
"smt2perr040.smt2"
"smt2perr041.smt2"
"smt2perr042.smt2"
"smt2perr043.smt2"
"smt2perr044.smt2"
"smt2perr045.smt2"
"smt2perr046.smt2"
"smt2perr047.smt2"
"smt2perr048.smt2"
"smt2perr049.smt2"
"smt2perr050.smt2"
"smt2perr051.smt2"
"smt2perr052.smt2"
"smt2perr053.smt2"
"smt2perr054.smt2"
"smt2perr055.smt2"
"smt2perr056.smt2"
"smt2perr057.smt2"
"smt2perr058.smt2"
"smt2perr059.smt2"
"smt2perr060.smt2"
"smt2perr061.smt2"
"smt2perr062.smt2"
"smt2perr063.smt2"
"smt2perr064.smt2"
"smt2perr065.smt2"
"smt2perr066.smt2"
"smt2perr067.smt2"
"smt2perr068.smt2"
"smt2perr069.smt2"
"smt2perr070.smt2"
"smt2perr071.smt2"
"smt2perr072.smt2"
"smt2perr073.smt2"
"smt2perr074.smt2"
"smt2perr075.smt2"
"smt2perr076.smt2"
"smt2perr077.smt2"
"smt2perr078.smt2"
"smt2perr079.smt2"
"smt2perr080.smt2"
"smt2perr081.smt2"
"smt2perr082.smt2"
"smt2perr083.smt2"
"smt2perr084.smt2"
"smt2perr085.smt2"
"smt2perr086.smt2"
"smt2perr087.smt2"
"smt2perr088.smt2"
"smt2perr089.smt2"
"smt2perr090.smt2"
"smt2perr091.smt2"
"smt2perr092.smt2"
"smt2perr093.smt2"
"smt2perr094.smt2"
"smt2perr095.smt2"
"smt2perr096.smt2"
"smt2perr097.smt2"
"smt2perr098.smt2"
"smt2perr099.smt2"
"smt2perr100.smt2"
"smt2perr101.smt2"
"smt2perr102.smt2"
"smt2perr103.smt2"
"smt2perr104.smt2"
"smt2perr105.smt2"
"smt2perr106.smt2"
"smt2perr107.smt2"
"smt2perr108.smt2"
"smt2perr109.smt2"
"smt2perr110.smt2"
"smt2perr111.smt2"
"smt2perr112.smt2"
"smt2perr113.smt2"
"smt2perr114.smt2"
"smt2perr115.smt2"
"smt2perr116.smt2"
"smt2perr117.smt2"
"smt2perr118.smt2"
"smt2perr119.smt2"
"smt2perr120.smt2"
"smt2perr121.smt2"
"smt2perr122.smt2"
"smt2perr123.smt2"
"smt2perr124.smt2"
"smt2perr125.smt2"
"smt2perr126.smt2"
"smt2perr127.smt2"
"smt2perr128.smt2"
"smt2perr129.smt2"
"smt2perr130.smt2"
"smt2perr131.smt2"
"smt2perr132.smt2"
"smt2perr133.smt2"
"smt2perr134.smt2"
"smt2perr135.smt2"
"smt2perr136.smt2"
"smt2perr137.smt2"
"smt2perr138.smt2"
"smt2perr139.smt2"
"smt2perr140.smt2"
"smt2perr141.smt2"
"smt2perr142.smt2"
"smt2perr143.smt2"
"smt2perr144.smt2"
"smt2perr145.smt2"
"smt2perr146.smt2"
"smt2perr147.smt2"
"smt2perr148.smt2"
"smt2perr149.smt2"
"smt2perr150.smt2"
"smt2perr151.smt2"
"smt2perr152.smt2"
"smt2perr153.smt2"
"smt2perr155.smt2"
"smt2perr156.smt2"
"smt2perr157.smt2"
"smt2perr158.smt2"
"smt2perr159.smt2"
"smt2perr160.smt2"
"smt2perr161.smt2"
"smt2perr162.smt2"
"smt2perr163.smt2"
"smt2perr164.smt2"
"smt2perr165.smt2"
"smt2perr166.smt2"
"smt2perr167.smt2"
"smt2perr168.smt2"
"smt2perr169.smt2"
"smt2perr170.smt2"
"smt2perr171.smt2"
"smt2perr172.smt2"
"smt2perr173.smt2"
"smt2perr174.smt2"
"smt2perr175.smt2"
"smt2perr176.smt2"
"smt2perr177.smt2"
"smt2perr178.smt2"
"smt2perr179.smt2"
)

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()

if(SymFPU_FOUND)
  list(APPEND sat_testcases
    "fp_to_fp.smt2"
    "fp_sort.smt2"
    "fp_regr1.smt2"
    "fp_regr2.smt2"
    "fp_regr3.smt2"
    "fp_regr4.smt2"
    "fp_regr6.smt2"
    "fp_regr7.smt2"
    "fp_regr8.smt2"
    "fp_regr10.smt2"
    "checkmodelfp1.smt2"
    "fp_regr11.smt2"
  )

  list(APPEND unsat_testcases
    "Float-no-simp1-main.smt2"
    "Float-no-simp3-main.smt2"
    "fp_inf.smt2"
    "fp_min.smt2"
    "fp_max.smt2"
    "fp_misc.smt2"
    "fp_nan.smt2"
    "fp_zero.smt2"
    "fp_fromsbv.smt2"
    "uf_fpmin.smt2"
    "uf_fpmax.smt2"
    "uf_toubv.smt2"
    "uf_tosbv.smt2"
  )

  list(APPEND cmp_testcases
    "fp_regr5.smt2 -i"
    "fp_regr9.smt2"
    "fp_real.smt2"
    "fp_rational.smt2"
  )
endif()



get_target_property(BITWUZLA_BINARY_PATH bitwuzla-bin RUNTIME_OUTPUT_DIRECTORY)
set(BITWUZLA_BINARY "${BITWUZLA_BINARY_PATH}/bitwuzla")
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}
      ${BITWUZLA_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()

if(PYTHON)
  add_subdirectory(python)
endif()